Inspired by this quesion, I'm trying to compute the derivative of the below function. Could you please verify if my proof looks fine or contains logical gaps/errors? Thank you so much for your help!
Let $X$ be a metric space and $F$ a normed vector space. Suppose $f_j: X \to \mathbb R$ is differentiable at $a$ for all $j = \overline{1,n}$ and $g: \mathbb R^n \to F$ is differentiable at $(f_1(a),\ldots, f_n(a))$. Prove that $g \circ (f_1,\ldots,f_m)$ is differentiable at $a$ and compute its derivative.
My attempt:
Lemma: Assume that $f_j:X \to E_j$ is differentiable at $a$ for all $j = \overline{1,n}$. Then $$\begin {array}{l|rcl} f & X & \longrightarrow & E_{1} \times \cdots \times E_{n} \\ & x & \longmapsto & (f_1 (x), \ldots, f_n(x)) \end{array}$$ is differentiable at $a$ and $\partial f(a) = (\partial f_1 (a), \ldots, \partial f_n(a))$.
Let $f = (f_1,\ldots,f_m)$. Then $g \circ (f_1,\ldots,f_m) = g \circ f$. It follows from our Lemma that $f$ is differentiable at $a$. By the chain rule and our Lemma, we get $$\begin{aligned} \partial (g \circ f) (a) &= \partial g (f(a) \circ \partial f (a) \\ &= \sum_{j=1}^n \partial_j g(f(a)) \cdot \partial f_j (a)\end{aligned}$$
Update:
Let $\{e_j \mid 1 \le j \le n\}$ be the standard basis of $\mathbb R^n$.
Because $g \circ f \in F^X$, $\partial (g \circ f)(a) \in \mathcal L(X,F)$. In other words,
$$\begin {array}{l|rcl} \partial (g \circ f)(a) & X & \longrightarrow & F \\ & x & \longmapsto & \partial (g \circ f)(a)(x) \end{array}$$
Similarly, we have
$$\begin {array}{l|rcl} \partial f_j(a) & X & \longrightarrow & \mathbb R \\ & x & \longmapsto & \partial f_j(a)(x) \end{array} \quad \text{and} \quad\begin {array}{l|rcl} \partial g(f(a)) & \mathbb R^n & \longrightarrow & F \\ & v & \longmapsto & \partial g(f(a))(v) \end{array}$$
We have $\partial g (f(a) \circ \partial f (a)$ is a continuous linear map such that
$$\begin {array}{l|rcl} \partial g (f(a) \circ \partial f (a) & X & \longrightarrow & \mathbb R \\ & x & \longmapsto & \left (\sum_{j=1}^n \partial_j g(f(a)) \cdot \partial f_j (a) \right )(x) = \sum_{j=1}^n \partial_j g(f(a)) \cdot \partial f_j (a) (x)\end{array}$$
Here $\partial f_j (a)(x) \in \mathbb R$ and $\partial_j g(f(a)) = \partial g(f(a)) (e_j) \in F$. Hence $\partial_j g(f(a)) \cdot \partial f_j (a) (x) \in F$ and thus $\sum_{j=1}^n \partial_j g(f(a)) \cdot \partial f_j (a) (x) \in F$.
The derivative of $g\circ f$ at $a$ should be $\sum_{j=1}^n \partial_j g(f(a)) \cdot \partial f_j$.
Notice that the function $g\circ f$ maps $X$ to $F$ so, for instance, if $F=\mathbb{R}$ and $n>1$ then the derivative of $g\circ f$ at $a$ is a real number whereas $\sum_j\partial_kg(f(a))\cdot\partial f_j(a)$ is an $n$-dimensional vector.