Test function operations are continuous

Differentiation does not enlarge support, and F4 gives $p_m({\mathrm{\partial }}^{\alpha }\phi )\le p_{m+\mathrm{\mid }\alpha \mathrm{\mid }}(\phi )$. Thus it is continuous on each fixed-support space. For products the one-coordinate product rule follows by subtracting $a(x)\phi (x)$ from $a(x+t{e}_i)\phi (x+t{e}_i)$, inserting $a(x+t{e}_i)\phi (x)$ and dividing by $t$; continuity and the derivative limits give the two terms. Induction using F4 and Pascal's identity then gives [given, F2, F4, algebra] ${\mathrm{\partial }}^{\beta }(a\phi )={\sum }_{\gamma \le \beta }\left(\genfrac{}{}{0px}{}{\beta }{\gamma }\right)({\mathrm{\partial }}^{\gamma }a)({\mathrm{\partial }}^{\beta -\gamma }\phi )\mathrm{.}$ All derivatives of $a$ through order $m$ are bounded on compact $K$, so $p_m(a\phi )\le 2^m{A}_{m,K}{p}_m(\phi )$, where $A_{m,K}={\max }_{\mathrm{\mid }\gamma \mathrm{\mid }\le m}{\sup }_K\mathrm{\mid }{\mathrm{\partial }}^{\gamma }a\mathrm{\mid }$. Support again stays in $K$.

Translation takes support into $K+h$ and preserves each derivative supremum. Its inverse is $T_{-h}$. Composition takes support into $L=F^{-1}(K)$, compact because it is the image of $K$ under the continuous inverse. The first derivative formula is ${\mathrm{\partial }}_i(\phi \circ F)={\sum }_j({\mathrm{\partial }}_j\phi )\circ F{\mathrm{\partial }}_i{F}_j$, by F3. Inductively, each derivative of order $\mathrm{\ell }\le m$ is a finite sum of $({\mathrm{\partial }}^{\beta }\phi )\circ F$, $\mathrm{\mid }\beta \mathrm{\mid }\le \mathrm{\ell }$, times products of derivatives of $F$ of orders at most $\mathrm{\ell }$: differentiating a term either differentiates its coefficient by the product rule of step 1.1 or raises $\beta$ by a coordinate using the first derivative formula. All coefficients are bounded on $L$, so $p_{m,L}(\phi \circ F)\le C_{m,K,F}{p}_{m,K}(\phi )$ for a finite constant.

The bounds in steps 1.1 and 2.1 prove continuity from each source stage into the indicated target stage. Composing with its continuous inclusion and applying F1 proves all asserted LF continuities. Apply the composition argument to $F^{-1}$ and the translation argument to $-h$ for continuous inverses. Empty support gives the zero test and all bounds hold with zero left side; the zero multi-index gives the identity map. Only finitely many derivative bounds are used for each estimate, so no choice axiom is needed. $\mathrm{\square }$