Proper smooth maps pull back compactly supported forms

The complement $N\setminus K$ is open by [F4], and $\omega$ vanishes identically there. Since $F$ is continuous by [F3], $U=F^{-1}(N\setminus K)$ is open. For $x\in U$, the pullback formula in [F2] evaluates ${\omega }_{F(x)}=0$ on the images under $d{F}_x$ of any tangent vectors, so $(F^{\ast }\omega {)}_x=0$. Thus the nonzero locus of $F^{\ast }\omega$ is contained in the closed set $M\setminus U=F^{-1}(K)$. Taking its closure and using [F4] proves the support containment. This step does not use properness.

Properness makes $F^{-1}(K)$ compact because $K$ is compact. The left-hand support $S$ in step 1.1 is closed in $M$. To verify its compactness, add $M\setminus S$ to any ambient open cover of $S$; this covers $F^{-1}(K)$. By [F5] take finitely many covering members and discard $M\setminus S$. The remaining finite family still covers $S$, so [F5] makes $S$ compact. Therefore $F^{\ast }\omega \in {\mathrm{\Omega }}_c^k(M)$ by [F1]. Linearity is the same pointwise linearity of [F2], restricted to these vector subspaces.

For $k<0$ or when the source form is forced to be zero by dimension, pullback is zero. In degree zero it is ordinary composition of functions, and step 1.1 applies unchanged; in degree one it evaluates $\omega$ on $d{F}_{x}v$. A rank-deficient or constant map may make the inclusion strict, which is harmless; no equality of supports was used. Empty manifolds and zero forms give empty supports. Boundary points are included in [F2], and properness still refers to compact sets in the whole manifold, including its boundary. Only one given compact support and a finite subcover were used, so no choice principle enters.