Integration descends to compactly supported top de Rham cohomology

Every top form is closed by [F1]. If $n\ge 1$ and another representative is $\omega +d\eta$ with $\eta \in {\mathrm{\Omega }}_c^{n-1}(M)$, linearity and compact Stokes in [F2] give ${\mathcal{I}}_M(\omega +d\eta )-{\mathcal{I}}_M(\omega )={\mathcal{I}}_M(d\eta )=0.$ Thus the displayed rule is independent of representatives in exactly the quotient [F1]. For $n=0$, the denominator is zero, so no negative-degree Stokes statement or primitive is needed.

For classes $[\omega ],[\zeta ]$ and scalars $a,b$, their quotient linear combination is represented by $a\omega +b\zeta$ by [F1]. By [F2], its value is $a{\mathcal{I}}_M(\omega )+b{\mathcal{I}}_M(\zeta )$. Hence ${\mathrm{Int}}_M$ is linear. It is defined by the common value of all representatives, not by choosing a representative for each class.

To compare with the earlier definition, now additionally assume [F6] and let $({\rho }_i,{\varphi }_i)$ be a global partition and charts allowed by [F3]. By [F5], only finitely many ${\rho }_i\omega$ are nonzero, and $\omega ={\sum }_i{\rho }_i\omega$ as a finite equality. Each summand has compact support contained in its chart. The chart-agreement and linearity clauses of [F2] therefore give ${\mathcal{I}}_M(\omega )={\sum }_i{\mathcal{I}}_M({\rho }_i\omega )={\sum }_i{I}_{{\varphi }_i}({\rho }_i\omega )={\int }_M\omega \text{in the sense of [F3].}$ For $n=0$ both definitions are the same finite signed point sum. Thus the comparison does not rely on a choice-free existence claim for a global partition. In this conditional setting, step 1.1 also agrees with the vanishing supplied by [F4].

Empty manifolds and zero forms give value zero. At $n=0$ the map acts on compactly supported functions with no quotient by negative forms; at $n=1$ the exactness comparison uses compactly supported function primitives and their zero endpoint differences. At every top degree the support requirement is on $\eta$, not just $d\eta$. The main quotient and linearity arguments use only [F1] and [F2] and are choice-free; countable choice is confined to the expressly conditional comparison in step 3.1. No assertion of injectivity or surjectivity has yet been made.