[proofplan] We use the definition of the second Frechet derivative as the Frechet derivative of the first derivative map. Near $a$, the [directional derivative](/page/Directional%20Derivative) in direction $v$ is the function $x \mapsto Df_x(v)$. Differentiating this function at $a$ in the direction $u$ amounts to composing the Frechet derivative of $Df$ at $a$ with the continuous evaluation map $L \mapsto L(v)$, which gives $D(Df)_a(u)(v)=D^2f_a(u,v)$. [/proofplan]

[step:Express the inner directional derivative through the first Frechet derivative] Choose an open neighbourhood $U_0 \subset U$ of $a$ such that $f$ is Frechet differentiable at every point of $U_0$ and \begin{align*} Df: U_0 &\to \mathcal{L}(\mathbb{R}^m,\mathbb{R}^n) \end{align*} is Frechet differentiable at $a$. Define the map \begin{align*} \phi: U_0 &\to \mathbb{R}^n \end{align*} \begin{align*} x &\mapsto Df_x(v). \end{align*} By the definition of the directional derivative induced by the Frechet derivative, for each $x \in U_0$, \begin{align*} D_v f(x)=Df_x(v)=\phi(x). \end{align*} Thus $D_uD_v f(a)$ exists exactly when the directional derivative $D_u\phi(a)$ exists, and in that case \begin{align*} D_uD_v f(a)=D_u\phi(a). \end{align*} [/step]

[step:Differentiate the evaluation of the derivative map]Let $|\cdot|$ denote the Euclidean norm on $\mathbb{R}^m$ and $\mathbb{R}^n$, and let $\|\cdot\|_{\mathrm{op}}$ denote the corresponding operator norm on $\mathcal{L}(\mathbb{R}^m,\mathbb{R}^n)$. Define the evaluation map at $v$ by \begin{align*} E_v: \mathcal{L}(\mathbb{R}^m,\mathbb{R}^n) &\to \mathbb{R}^n \end{align*} \begin{align*} L &\mapsto L(v). \end{align*} The map $E_v$ is linear, and for every $L \in \mathcal{L}(\mathbb{R}^m,\mathbb{R}^n)$, \begin{align*} |E_v(L)|=|L(v)| \leq \|L\|_{\mathrm{op}} |v|, \end{align*} so $E_v$ is continuous. Then $\phi=E_v \circ Df$ on $U_0$. Since $Df$ is Frechet differentiable at $a$ and $E_v$ is continuous linear, the composition $E_v \circ Df$ is Frechet differentiable at $a$, with derivative \begin{align*} D\phi_a = E_v \circ D(Df)_a. \end{align*} Therefore the directional derivative of $\phi$ at $a$ in the direction $u$ exists and satisfies \begin{align*} D_u\phi(a)=D\phi_a(u)=E_v(D(Df)_a(u))=D(Df)_a(u)(v). \end{align*}[/step]

[guided]The function whose directional derivative we must compute is not $f$ itself, but the function obtained after first differentiating $f$ in direction $v$. On the neighbourhood $U_0$, the first Frechet derivative exists at every point, so the inner directional derivative is the map \begin{align*} \phi: U_0 &\to \mathbb{R}^n \end{align*} \begin{align*} x &\mapsto Df_x(v). \end{align*} The useful way to view $\phi$ is as a composition. First send $x$ to the [linear map](/page/Linear%20Map) $Df_x \in \mathcal{L}(\mathbb{R}^m,\mathbb{R}^n)$, and then evaluate that linear map at the fixed vector $v$. Define \begin{align*} E_v: \mathcal{L}(\mathbb{R}^m,\mathbb{R}^n) &\to \mathbb{R}^n \end{align*} \begin{align*} L &\mapsto L(v). \end{align*} Let $|\cdot|$ denote the Euclidean norm on $\mathbb{R}^m$ and $\mathbb{R}^n$, and let $\|\cdot\|_{\mathrm{op}}$ denote the corresponding operator norm on $\mathcal{L}(\mathbb{R}^m,\mathbb{R}^n)$. This map is linear because evaluation of linear maps at a fixed vector respects addition and scalar multiplication. It is continuous because \begin{align*} |E_v(L)|=|L(v)| \leq \|L\|_{\mathrm{op}} |v| \end{align*} for every $L \in \mathcal{L}(\mathbb{R}^m,\mathbb{R}^n)$. Hence $\|E_v\|_{\mathrm{op}} \leq |v|$. Now $\phi=E_v \circ Df$. The hypothesis that $f$ is twice Frechet differentiable at $a$ means precisely that the derivative map $Df: U_0 \to \mathcal{L}(\mathbb{R}^m,\mathbb{R}^n)$ is Frechet differentiable at $a$. Since $E_v$ is continuous linear, composing with $E_v$ preserves Frechet differentiability at $a$, and the derivative is obtained by composing derivatives: \begin{align*} D\phi_a=E_v \circ D(Df)_a. \end{align*} Evaluating this derivative on the direction $u$ gives \begin{align*} D_u\phi(a)=D\phi_a(u)=E_v(D(Df)_a(u))=D(Df)_a(u)(v). \end{align*} Thus the outer directional derivative exists, and it is exactly the derivative of $Df$ at $a$ in direction $u$, evaluated at the vector $v$.[/guided]

[step:Identify the resulting bilinear expression with the second Frechet derivative] By the convention stated in the theorem, the second Frechet derivative at $a$ is the bilinear map \begin{align*} D^2f_a: \mathbb{R}^m \times \mathbb{R}^m &\to \mathbb{R}^n \end{align*} defined by \begin{align*} D^2f_a(u,v)=D(Df)_a(u)(v). \end{align*} Combining this identity with the computation above gives \begin{align*} D_uD_v f(a)=D_u\phi(a)=D(Df)_a(u)(v)=D^2f_a(u,v). \end{align*} This proves that $D_uD_v f(a)$ exists and has the asserted value. [/step]