The de Rham theorem

The source product descends by [F2], including the explicit simultaneous representative-change formula in its proof. The associative and graded-commutative wedge identities of [F8] hold pointwise in boundary charts by restricting their Euclidean extensions, as permitted in [F7]. They therefore descend to the quotient; the constant function $1$ is closed and is a wedge unit. Thus [F6] extends to the boundary convention with exactly the same product and unit. Finite sums of homogeneous classes multiply into the direct sum by finite distributivity. The continuous target is the algebra of [F3].

Restriction respects cup already on cochains. Indeed, for continuous cochains $u$ of degree $p$ and $v$ of degree $q$, evaluation on a smooth $(p+q)$-simplex gives $r(u⌣v)(\sigma )=u(\sigma [0,\dots ,p])v(\sigma [p,\dots ,p+q])=((ru)⌣(rv))(\sigma )\mathrm{.}$ Every displayed face is smooth. Restriction also sends the constant-vertex cochain of value one to the same smooth cochain, so it preserves the unit. These identities descend to classes by [F3] and its smooth version.

For homogeneous source classes $a,b$, equations [F1], [F2] and step 1.2 give $r(J(ab))=I(ab)=I(a)⌣I(b)=r(J(a))⌣r(J(b))=r(J(a)⌣J(b))\mathrm{.}$ The map $r$ is injective by [F1], so $J(ab)=J(a)⌣J(b)$. Integration of the constant function one on a vertex is one; hence $I([1])=r(\mathbf{1})$ and injectivity gives $J([1])=\mathbf{1}$. Degreewise linearity and finite distributivity now make $J$ a unital graded real-algebra homomorphism on the direct sum.

The degreewise inverses in [F1] take a finite list of homogeneous components to a finite list, so their direct sum is the inverse of $J$. Its multiplicativity also follows directly: writing any $x,y$ in the target as $J(a),J(b)$ gives $J^{-1}(xy)=J^{-1}(J(ab))=ab$, and the same argument preserves the unit. The resulting isomorphism is natural by the actual smooth-map naturality in [F1]. For homogeneous degrees $p,q$, the source wedge sign from step 1.1 and the target cup sign from [F4] coincide; only the cohomology product, not the cochain cup, is asserted graded commutative.

The empty manifold gives the zero unital algebra on both sides, with $1=0$. A point and degree zero use the vertex-unit calculation; degree one, top degree and negative zero groups are included in [F1]. No finite-support condition on components is imposed in degree zero: the unit assigns one to every vertex even on a disconnected manifold. Smooth degenerate simplices were retained in [F2] and step 1.2. The only choice assumption is [F5] inherited by the degreewise bijectivity in [F1]; the multiplication, unit and cancellation calculations add no selections. Thus neither compactness nor full AC has entered the theorem.