> [!theorem] > > Let $X$ and $Y$ be $C^p$-[[Manifold|manifolds]] ($p \ge 1$) modelled on the [[Banach Space|Banach spaces]] $E$ and $F$, respectively. Let $f: X \to Y$ be a $C^p$-[[Manifold Morphism|morphism]], and $(U, \psi) \in X$, $(V, \varphi) \in Y$ such that $\varphi \circ f \circ \psi^{-1}$ is of class [$C^p$](Space%20of%20Continuously%20Differentiable%20Functions). > > Define > $ > df(p): T_pX \to T_pY > $ > with > $ > \ol{h} \mapsto \ol{Df_{U, V}(\hat{p})(h)} > $ > where the bar refers to the corresponding [[Equivalence Class|equivalence classes]], then $df(p)$ is well-defined at $p$. > > *Proof*. Let $(U_1, \psi_1)$, $(V_1, \varphi_1)$ and $(U_2, \psi_2)$, $(V_2, \varphi_2)$ be two pairs of [[Atlas|charts]] with $p \in U_1, U_2$ and $f(p) \in V_1, V_2$ such that $\varphi_1 \circ f \circ \psi_1^{-1}$ and $\varphi_2 \circ f \circ \psi_2^{-1}$ are $C^p$ morphisms. > > Let $h \in T_{(U_1, \psi_1, p)}X$, then $\braks{D(\psi_2 \circ \psi_1^{-1})(\psi_1(p))}(h)$ is the unique vector in $T_{(U_2, \psi_2, p)}$ equivalent to $h$. In which case, by the [[Chain Rule|chain rule]] > $ > \begin{align*} > &\braks{Df_{U_2, V_2}(\psi_2(p))} \circ \braks{D(\psi_2 \circ \psi_1^{-1})(\psi_1(p))}(h) \\ > &=\paren{D\braks{(f_{U_2, V_2}) \circ (\psi_2 \circ \psi_1^{-1})}(\psi_1(p))}(h) \\ > &=\paren{D\braks{(\varphi_2 \circ f \circ \psi_2^{-1}) \circ (\psi_2 \circ \psi_1^{-1})}(\psi_1(p))}(h) \\ > &=\paren{D\braks{(\varphi_2 \circ f \circ \psi_1^{-1})}(\psi_1(p))}(h) \\ > &= \braks{D(f_{U_2,V_1})(\psi_1(p))}(h) \in T_{(V_2, \varphi_2, f(p))}Y > \end{align*} > $ > Now, > $ > \braks{D(\varphi_1 \circ \varphi_2^{-1})(\varphi_2(p))} \circ \braks{D(f_{U_2,V_1})(\psi_1(p))}(h) > $ > is the unique vector in $T_{(V_1, \varphi_1, f(p))}Y$ equivalent to $\braks{D(f_{U_2,V_1})(\psi_1(p))}(h)$. By the chain rule again, > $ > \begin{align*} > &\braks{Df_{U_2, V_2}(\psi_2(p))} \circ \braks{D(\psi_2 \circ \psi_1^{-1})(\psi_1(p))}(h) \\ > &\sim \braks{D(\varphi_1 \circ \varphi_2^{-1})(\varphi_2(p))} \circ \braks{D(f_{U_2,V_1})(\psi_1(p))}(h) \\ > &= \paren{D\braks{(\varphi_1 \circ \varphi_2^{-1}) \circ (\varphi_2 \circ f \circ \psi_1^{-1})}(\psi_1(p))}(h) \\ > &= \braks{D(\varphi_1 \circ f \circ \psi_1^{-1})(\psi_1(p))}(h) \\ > &= \braks{D(f_{U_1, V_1})(\psi_1(p))}(h) > \end{align*} > $ > As equivalent concrete tangent vectors get mapped to equivalent concrete tangent vectors, the differential between the [[Tangent Space|tangent spaces]] is well-defined.