Frechet derivative of compact operator is compact ... this seems to be a well known fact as mentioned in this and in this manuscript. 
However, I was not able to find a proof or to prove it by myself.
So my question is: How to prove this?
Any hint or reference is appreciated.
 A: Theorem. Let $\Omega$ be an open set in a Banach space $X$ and let $F \in C(\Omega,X)$. If the Fréchet derivative $F'(x_0)$ exists for some $x_0\in\Omega$, then $F'(x_0)$ is a (linear) compact operator.
Proof. Assume that $F'(x_0)$ is not compact. Then one can find $\epsilon_0>0$ and a sequence $\{y_n\}_n$ such that $\|y_n\|\leq 1$ and 
$$
\|F'(x_0)y_k - F'(x_0)y_l\| \geq \epsilon_0
$$
for $k \neq l$. By definition of the Fréchet derivative, there is $\delta>0$ such that
$$
\|F(x_0+h)-F(x_0)-F'(x_0)h\| \leq \frac{\epsilon_0}{4}\|h\|
$$
provided that $\|h\| < \delta$. Choose $\tau$ such that $\|\tau y_k\|<\delta$ and $x_0+\tau y_k \in \Omega$ for all $k \in \mathbb{N}$. Then
$$
\begin{split}
\|F(x_0+\tau y_k)-F(x_0+\tau y_l)\| & \geq \|F'(x_0) (\tau y_k-\tau y_l)\|-\|F(x_0+\tau y_k)-F(x_0)-F'(x_0)\tau y_k\| \\
&{}-\|F(x_0+\tau y_l)-F(x_0)-F'(x_0)\tau y_l\| \geq \frac{\epsilon_0}{2}\tau.
\end{split}
$$ 
But this means that $F$ is not compact on $\Omega$, a contradiction. QED.
Another proof appears in Deimling's book on nonlinear functional analysis. However, it is based on the measure of non-compactness, and it is therefore less direct.
