Closed bounded test function sets are compact

Empty $B$ is compact. Otherwise F1 gives compact $K\subseteq \mathrm{\Omega }$ containing all supports, with $M_m={\sup }_{f\in B}{p}_m(f)<\mathrm{\infty }$. Regard the tests as globally smooth zero extensions and choose a nondegenerate closed box $Q$ whose interior contains $K$. For every multi-index $\alpha$, the real and imaginary parts of ${\mathrm{\partial }}^{\alpha }f{\mathrm{\mid }}_Q$, $f\in B$, are uniformly bounded by $M_{\mathrm{\mid }\alpha \mathrm{\mid }}$. Their segment derivatives have norm at most $\sqrt{n}{M}_{\mathrm{\mid }\alpha \mathrm{\mid }+1}$ times the segment direction norm. F6 therefore gives a common Lipschitz bound on $Q$, proving equicontinuity. F3 applies to each real family.

Fix $\epsilon >0$ and choose $N$ with ${\sum }_{m>N}{2}^{-m-1}<\epsilon \mathrm{/}2$. For each of the finitely many real and imaginary derivative families through order $N$, F3 and F4 give a finite sup-norm $\delta$-net, with $0<\delta <\epsilon \mathrm{/}8$. Assign each $f\in B$ the first net center within $\delta$ for each coordinate, using fixed finite listings. There are finitely many joint labels. Choose one member of each nonempty label class. If $f,g$ have the same label, their real and imaginary derivative differences through order $N$ are each less than $2\delta$, so $p_N(f-g)<4\delta <\epsilon \mathrm{/}2$. F2's metric then gives $d(f,g)<\epsilon$. The finitely many representatives form an $\epsilon$-net for $B$, proving total boundedness without an infinite diagonal selection.

By F5 the inverse image of the LF-closed set $B$ in ${\mathcal{D}}_K$ is closed; it is just $B$. A Cauchy sequence in $B$ converges in ${\mathcal{D}}_K$ by F2 and its limit belongs to $B$ by closedness. Thus $B$ is complete. F4 and step 2.1 imply metric compactness in ${\mathcal{D}}_K$. For any LF-open cover of $B$, inverse images under F5 give a stage-open cover; a finite subcover there is a finite subcover in the LF space. This proves the required compactness. If $K$ has empty interior, all its tests vanish and $B$ is a subset of the singleton zero space. F7 is used through F3 and F4, with no stronger choice. $\mathrm{\square }$