Distributional differentiation is continuous and commutes

Evaluating consecutive derivatives on a test gives $(-1{)}^{\mathrm{\mid }\alpha \mathrm{\mid }+\mathrm{\mid }\beta \mathrm{\mid }}u({\mathrm{\partial }}^{\beta }{\mathrm{\partial }}^{\alpha }\phi )$. By F4 this is $(-1{)}^{\mathrm{\mid }\alpha +\beta \mathrm{\mid }}u({\mathrm{\partial }}^{\alpha +\beta }\phi )$, which is ${\mathrm{\partial }}^{\alpha +\beta }u(\phi )$ by F1. Linearity follows from the same formula.

For a single test $\phi$, the weak seminorm of ${\mathrm{\partial }}^{\alpha }u$ equals $\mathrm{\mid }u({\mathrm{\partial }}^{\alpha }\phi )\mathrm{\mid }$, a weak seminorm of $u$. For a bounded test set $B$, the set ${\mathrm{\partial }}^{\alpha }B$ is bounded: any zero-neighborhood has a zero-neighborhood inverse image under the continuous linear test derivative of F3, and absorption of $B$ by that inverse image gives absorption of its image. Hence $p_B({\mathrm{\partial }}^{\alpha }u)=p_{{\mathrm{\partial }}^{\alpha }B}(u)$, a strong seminorm. These equalities prove continuity in both topologies, including for nets, without choice.

Now assume F10 and $f\in C^1(\mathrm{\Omega };\mathbb{C})$, and fix a test $\phi$. Use F6 to choose $\chi =1$ near $\mathrm{supp}\phi$ with compact support in $\mathrm{\Omega }$. Extend $g=\chi f$ by zero to ${\mathbb{R}}^n$; it is $C^1$ because it vanishes near the complement of $\mathrm{\Omega }$. Choose a nondegenerate box containing the supports of $g$ and $\phi$ in its interior. On each coordinate segment F7 gives $\int g{\mathrm{\partial }}_i\phi =-\int ({\mathrm{\partial }}_{i}g)\phi$, because $\phi$ is zero at both endpoints. For complex functions expand into real and imaginary parts and apply the real identity to the four products. All integrands and sections are continuous on compact boxes and are Riemann integrable: uniform continuity makes their oscillation Darboux sums arbitrarily small on sufficiently fine uniform grids. For $n>1$, F8 integrates the one-coordinate identity over the remaining coordinates; for $n=1$ this is already the required identity. F9 componentwise converts the two multiple Riemann integrals to Lebesgue integrals. Near the test support $g=f$ and ${\mathrm{\partial }}_{i}g={\mathrm{\partial }}_{i}f$, so the resulting equality is $-{\int }_{\mathrm{\Omega }}f{\mathrm{\partial }}_i\phi ={\int }_{\mathrm{\Omega }}({\mathrm{\partial }}_{i}f)\phi$.

Continuous functions and their continuous derivatives are locally integrable by compact boundedness, and their regular functionals are continuous since their absolute pairings are bounded by ${\int }_K\mathrm{\mid }f\mathrm{\mid }{p}_0$ on each fixed support (or directly by the global $Q_0$ seminorm on that stage). F5 and step 3.1 therefore give ${\mathrm{\partial }}_i{u}_f=u_{{\mathrm{\partial }}_{i}f}$. Iterating this identity through at most $k$ derivatives for $f\in C^k$, and using step 1.1, proves the classical-compatibility formula. Degree zero is the identity. Zero functions and the empty domain give zero distributions. The additional axiom enters only through the integral comparison in the classical argument; the algebra and dual continuity remain choice-free. $\mathrm{\square }$