The de Rham map is an isomorphism on a two-open union

Use the five consecutive terms of the exact de Rham row [F5] and smooth singular row [F6]: $H^{q-1}(U)\oplus H^{q-1}(V)⟶H^{q-1}(W)⟶H^q(M)⟶H^q(U)\oplus H^q(V)⟶H^q(W)\mathrm{.}$ The vertical maps are integration, with the direct sum of its two component maps at the first and fourth terms. Naturality [F7] gives both restriction squares, and naturality plus linearity gives the $V-U$ difference squares; in the countable-choice branch these are also the squares recorded in [F1]. The actual-small-chain identification in [F6] does not change these equalities: restriction of a global integration cochain to a small simplex in an open set is its integral there. The connector square commutes by [F2]. These are real vector spaces, hence modules over $\mathbb{R}$.

The first and fourth vertical maps are isomorphisms: the direct sum of the two hypothesized inverse integration maps is their inverse. The second and fifth vertical maps are the hypothesized isomorphisms on $W$ in degrees $q-1$ and $q$. Thus all four outside vertical maps in step 1.1 are isomorphisms. Applying [F3] proves the middle map $I_M:H_{\mathrm{d}\mathrm{R}}^q(M)\to H_{\mathrm{\infty }}^q(M;\mathbb{R})$ is both injective and surjective.

At $q=0$ the first two terms in each row are zero because the groups in degree minus one vanish; their vertical maps are the unique isomorphisms $0\to 0$. The initial injections in [F5] and [F6] give exactness at the middle term, so the same five-lemma application applies. In negative degrees both groups on $M$ are zero. This proves the conclusion in every integer degree, including $q=1$ and the top form degree, without assuming any higher singular group vanishes beforehand.

Empty opens or overlap produce zero terms, and $U=V=M$ produces diagonal and difference arrows; the same exact rows and proof cover these cases, including a point or the empty manifold. No chains are normalized or simplices discarded in [F6]. Assumption [F4] is used only to obtain the partition underlying the form row and its connector. With a partition supplied, [F5] gives the exact form row and [F2] gives connector compatibility choice-free; the other squares are the direct cochain equalities from [F7]. The five-lemma argument uses the specified inverse maps and no new choice.