Proposition 2 ("Leibniz' formula")

Let $E, F, G$ be three topological vector spaces over $\mathbf{R}$, and $(x, y) \mapsto [x.y]$ a continuous bilinear mapping of $E \times F$ into $G$. If $f$ (resp. $g$) is defined on an interval $I \subset \mathbf{R}$, takes its values in $E$ (resp. $F$) and has an $n^{th}$ derivative on $I$, then $[f.g]$ has an $n^{th}$ derivative on $I$, given by the formula

Formula (4) is proved by induction on $n$ (using the relation $\binom{n}{p} = \binom{n-1}{p} + \binom{n-1}{p-1}$ for the binomial coefficients).

In the same way one can verify the following formula (where the hypotheses are the same as in prop. 2):

The preceding propositions have been stated for functions that are $n$ times differentiable on an interval; we leave it to the reader to formulate the analogous propositions for functions that are $n$ times differentiable at a point.