Differentiability into the explicit disk through its ambient inclusion

For every natural number $m$, including $m=0$, let $E=\mathbb R^{m+1}$ with its Euclidean norm, $D=\{x\in E:\|x\|\leq1\}$, and $S^m=\{u\in E:\|u\|=1\}$, with their subspace topologies. The specified charted structure on $D$ has model half-space $H=\{y\in E:y_0\geq0\}$ and atlas consisting of the chart $x\mapsto x+2e_0$ on $\|x\|<1$ and, for each $p\in S^m$, the chart $x\mapsto(1-\|x\|,\sigma_{-p}(x/\|x\|))$ on $x\neq0$ and $x\neq-\|x\|p$, with target $\{y\in H:y_0<1\}$; $\sigma_{-p}$ is stereographic projection from $-p$, followed by the linear isometry to $\mathbb R^m$ chosen in the imported sphere construction. The preferred chart at $a$ is the first chart if $\|a\|<1$, and the boundary chart with $p=a$ if $\|a\|=1$. For every $k\in\mathbb N\cup\{\infty,\omega\}$, every real normed vector space $E'$, every topological space $H'$, every real model with corners $I:H'\to E'$, every topological space $M$ equipped with charts modeled on $H'$ whose transition maps satisfy the $C^k$ manifold condition for $I$, and every function $f:M\to D$, the function $f$ is $C^k$ from the model $I$ to the stated disk half-space model if and only if both $f$ is continuous as a function into the subspace $D$ and the function $a\mapsto f(a)$ regarded as $E$-valued is $C^k$ from $I$ to the identity model on $E$. The two conditions on the right are a conjunction. The order $k$ includes zero, every positive finite order, $\infty$ for smoothness, and $\omega$ for analytic chart regularity. The statement does not impose completeness or finite dimension on $E'$, or separation, countability, or nonemptiness hypotheses on $M$; an empty $M$ is included.