[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*}
[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]
[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]
