... 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.
Copyright © 2021 JogjaFile Inc.
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.