Post-composition with a C¹ map is a C¹ operator between spaces of continuous maps on a compact space

Let $X$ be a compact topological space, let $E$ and $F$ be real normed spaces, and let $v:E\to F$ be a map of class C¹. Write $C(X,E)$ for the space of continuous maps $X\to E$ with the supremum norm. Then the composition operator

is of class C¹.

In words: post-composition with a C¹ map is a C¹ map between spaces of continuous functions on a compact space (the composition operator, also called the Nemytskii operator). Its derivative at $\beta$ is $h\mapsto\big(s\mapsto Dv(\beta(s))\,h(s)\big)$. A general fact of analysis, not stated in the paper. In this mission it is a step in the proof of the companion theorem exists_localFlow_contMDiff_of_isInteriorPoint. That theorem says that the local flow of a C¹ vector field at an interior point is jointly C¹ in the initial point and the time. The proof of Proposition 1.1 (Section 3.1 of arXiv v1) uses it tacitly. There $X$ is a compact time interval and $N_v$ is the nonlinear part of the Picard operator $\beta\mapsto x+\tau\int_0^{\cdot} v(\beta)$.

Formalization Note $C(X,E)$ is Mathlib's C(X, E) (ContinuousMap) with the norm that exists for compact $X$. The operator is written fun β => ⟨v ∘ β, _⟩, where the second component is the proof that $v\circ\beta$ is continuous. No completeness and no finite dimension is assumed. Mathlib (at the pinned version) has the linear case only (ContinuousLinearMap.compLeftContinuous).