Good evening, I'm trying to prove this well-known theorem about Fréchet derivative:
$\textbf{Theorem:}$ Let $E,F$ be Banach spaces and $X$ open in $E$. Assume $m \ge 2$ and $f: X \to F$ such that $\partial^m f(a)$ exists. Then $$\partial^m f(a) \in \mathcal L_\text{sym}^m (E,F)$$
Could you please verify if my proof looks fine or contains logical gaps/errors? Thank you so much for your help!
$\textbf{My attempt:}$ I utilize two below lemmas in my proof:
$\textbf{Lemma 1:}$ Let $E,F$ be Banach spaces and $X$ open in $E$. Suppose $f:E \to F$ such that $\partial^2 f(a)$ exists. Then $\partial^2 f(a) \in \mathcal L_\text{sym}^2 (E,F)$.
$\textbf{Lemma 2:}$ Let $E,F$ be Banach spaces and $X$ open in $E$. Suppose $f: X \to \mathcal L^m (E,F)$ such that $f(X) \subseteq \mathcal L_\text{sym}^m (E,F)$ and that $f$ is differentiable at $a \in X$. Then $\partial f (a) [h_1] \in \mathcal L_\text{sym}^m (E,F)$ for all $h_1 \in E$.
Next we proceed to prove this theorem by induction on $m$ as follows. The base case $m=2$ holds by $\textbf{Lemma 1}$. Let it holds for $m$. Our goal is to prove that it holds for $m+1$.
By inductive hypothesis, $\partial^m f (a) \in \mathcal L_\text{sym}^m (E,F)$. In other words, we have $$\begin {array}{l|rcl} \partial^m f (a) & E^m & \longrightarrow & F \\ & [h_1, \ldots, h_m] & \longmapsto & \partial^m f (a) [h_1, \ldots, h_m] \end{array}$$ where $\partial^m f (a) [h_1, \ldots, h_m] = \partial^m f (a) [h_{\sigma(1)}, \ldots, h_{\sigma(m)}]$ for any permutation $\sigma$ of $\{1, \ldots,m \}$.
Because $\partial^{m+1} f (a)$ exists, there is a neighborhood $\mathcal U$ of $a$ such that $\partial^m f (x)$ exists for all $x \in \mathcal U$. As such, the map $$\begin {array}{l|rcl} \partial^m f & \mathcal U & \longrightarrow & \mathcal L^m (E,F) \\ & x & \longmapsto & \partial^m f (x) \end{array}$$
is well defined. By inductive hypothesis, $\partial^m f (\mathcal U) \subseteq \mathcal L_\text{sym}^m (E,F)$. It follows from $\textbf{Lemma 2}$ that $\partial (\partial^m f) (a) [h_1] = \partial^{m+1} f (a) [h_1] \in \mathcal L_\text{sym}^m (E,F)$ for all $h_1 \in E$. It follows that $$\partial^{m+1} f (a) [h_1,h_2, \ldots,h_m] = \partial^{m+1} f (a) [h_1, h_{\sigma(2)}, \ldots, h_{\sigma(2)}]$$
Our goal is done if we show that $$\partial^{m+1} f (a) [h_1,h_2,h_3, \ldots,h_m] = \partial^{m+1} f (a) [h_2, h_1,h_3, \ldots, h_{m+1}]$$
This statement is actually true due to $\textbf{Lemma 1}$ and $$\begin{aligned} \partial^{m+1} f (a) [h_1,h_2,h_3, \ldots,h_m] &= \partial^2( \partial^{m-1} f) (a) [h_1,h_2,h_3, \ldots,h_m] \\ &= \partial^2( \partial^{m-1} f)(a) [h_2, h_1,h_3, \ldots, h_{m+1}] \\ &= \partial^{m+1} f(a) [h_2, h_1,h_3, \ldots, h_{m+1}]\end{aligned}$$
This completes the proof.