I would like to check whether these proofs of the elementary claims below are valid. Trying to get used to this setting and these claims are so elementary that I haven't found them shown online. Just want to check that I am doing things correctly. Any pedantic feedback is appreciated.
Let $E$ and $F$ be Banach spaces with $U\subset E$ open. A continuous map $f:U\to F$ is $\textbf{(Frech\'et) differentiable}$ at $x_0\in U$ if there exists a continuous linear map $Df(x_0)\in L(E,F)$ such that $$f(x_0+h)-f(x_0)-Df(x_0)h=o(h),\qquad \lim_{|h|\to0}\frac{o(h)}{|h|}=0.$$ If $f$ is differentiable at every point in $U$, then $Df$ is a map $$Df:U\to L(E,F).$$
$\textbf{Lemma 1}$ Let $f:E\to F$ be a continuous linear map between Banach spaces $E$ and $F$. Then for each $x\in E$, $Df(x)=f$.
$\textit{Proof:}$ For any $x\in E$, let $Df(x):E\to L(E,F)$ be the map $h\mapsto f(h)$. Then since $f$ is linear, $f(x+h)-f(x)-Df(x)h=f(h)-Df(x)h=0.$ This shows $f$ is differentiable and $Df(x)=f.$ $\blacksquare$
$\textbf{Lemma 2}$ Let $E$ be a compact Banach space. The multiplication map $$m:C^l(E)\times C^k(E) \to C^k(E),\qquad (f,g)\mapsto fg$$ is smooth when $l\geq k\geq0.$
$\textit{Proof:}$ Fix $f\in C^l(E)$ and consider the continuous linear map $m_f:C^k(E) \to C^k(E)$ sending $g\mapsto fg.$ By Lemma $1$, we have $Dm_f(g)=m_f$. Hence, $m_f:C^k(E) \to C^k(E)$ is of class $C^1$. It follows by induction that $m_f$ is smooth. Since this holds for any $f\in C^l(E)$, the multiplication map $m$ is smooth. $\blacksquare$