[proofplan] We define the cross product $\Phi^k$ and verify it is a well-defined chain-level map. We then prove the theorem by induction on the size $p$ of a finite good cover of $M$. The base case $p = 1$ reduces, via the Poincaré Lemma and homotopy invariance, to the elementary identity $H^k(N) \cong \mathbb{R} \otimes H^k(N)$. For the inductive step we split $M$ along the last [open set](/page/Open%20Set) of the good cover and run the Mayer–Vietoris sequences for $M$ and for $M \times N$ in parallel, tensoring the former with $H^*(N)$. Tensoring with $H^*(N)$ preserves exactness because we work over the field $\mathbb{R}$. The [five lemma](/theorems/1938) applied to the resulting commutative ladder propagates the isomorphism from the pieces $U = U_1 \cup \cdots \cup U_{p-1}$, $V = U_p$, and $U \cap V$ (each of which has a good cover of size at most $p - 1$) to $M = U \cup V$. [/proofplan]

[step:Define the cross product and verify it descends to cohomology]Write $\Omega^\bullet(X)$ for the de Rham complex of smooth differential forms on a manifold $X$ with [exterior derivative](/theorems/1525) $d_X$. Define the **wedge cross product** on forms by \begin{align*} \times : \Omega^i(M) \otimes_{\mathbb{R}} \Omega^j(N) &\to \Omega^{i+j}(M \times N) \\ \omega \otimes \eta &\mapsto \pi_M^* \omega \wedge \pi_N^* \eta . \end{align*} Because pullback commutes with $d$ and the Leibniz rule holds on $\Omega^\bullet(M \times N)$, we compute for $\omega \in \Omega^i(M)$, $\eta \in \Omega^j(N)$: \begin{align*} d_{M \times N}(\pi_M^* \omega \wedge \pi_N^* \eta) &= \pi_M^*(d_M \omega) \wedge \pi_N^* \eta + (-1)^i \pi_M^* \omega \wedge \pi_N^*(d_N \eta). \end{align*} Hence if $\omega$ and $\eta$ are closed then so is $\pi_M^* \omega \wedge \pi_N^* \eta$, and if either is exact then $\pi_M^* \omega \wedge \pi_N^* \eta$ is exact. The induced map on cohomology \begin{align*} \Phi^k : \bigoplus_{i+j=k} H^i_{\mathrm{dR}}(M) \otimes_{\mathbb{R}} H^j_{\mathrm{dR}}(N) \to H^k_{\mathrm{dR}}(M \times N), \quad [\omega] \otimes [\eta] \mapsto [\pi_M^* \omega \wedge \pi_N^* \eta] \end{align*} is therefore well-defined and $\mathbb{R}$-linear in each tensor slot, hence factors through the [tensor product](/page/Tensor%20Product). For naturality, let $f : M' \to M$ and $g : N' \to N$ be smooth maps. The projection identities $\pi_M \circ (f \times g) = f \circ \pi_{M'}$ and $\pi_N \circ (f \times g) = g \circ \pi_{N'}$, combined with functoriality of pullback and compatibility of pullback with the wedge product, give $(f \times g)^*(\pi_M^* \omega \wedge \pi_N^* \eta) = \pi_{M'}^*(f^* \omega) \wedge \pi_{N'}^*(g^* \eta)$, which is the form-level identity $(f \times g)^* \circ \Phi^k_{M,N} = \Phi^k_{M',N'} \circ (f^* \otimes g^*)$. Descent to cohomology yields the corresponding naturality square.[/step]

[guided]We must produce a map *from* the right-hand side *to* the left, and verify it descends from forms to cohomology classes. The natural candidate is the wedge of the two pullbacks, since wedge is the only natural bilinear operation $\Omega^i \times \Omega^j \to \Omega^{i+j}$ on a single manifold, and pullback is the only natural way to ship forms from $M$ and $N$ to $M \times N$. To check this descends to cohomology, we need two facts: closed-times-closed is closed, and closed-times-exact is exact. Both follow from the Leibniz rule and the commutation $d \circ \pi_X^* = \pi_X^* \circ d_X$. Pulling back, applying $d_{M \times N}$, and using that $\pi_M^* \omega$ depends only on $M$-coordinates and $\pi_N^* \eta$ depends only on $N$-coordinates: \begin{align*} d_{M \times N}(\pi_M^* \omega \wedge \pi_N^* \eta) &= d_{M \times N}(\pi_M^* \omega) \wedge \pi_N^* \eta + (-1)^i \pi_M^* \omega \wedge d_{M \times N}(\pi_N^* \eta) \\ &= \pi_M^*(d_M \omega) \wedge \pi_N^* \eta + (-1)^i \pi_M^* \omega \wedge \pi_N^*(d_N \eta). \end{align*} If $d_M \omega = 0$ and $d_N \eta = 0$, the RHS vanishes, so the product is closed. If $\omega = d_M \alpha$, the product equals $d_{M \times N}(\pi_M^* \alpha \wedge \pi_N^* \eta)$ up to sign (using $d_N \eta = 0$), hence is exact. The case where $\eta$ is exact is symmetric. Because the wedge cross product is $\mathbb{R}$-bilinear on closed forms and vanishes on exact-times-closed pairs, the universal property of the [tensor product](/page/Tensor%20Product) over $\mathbb{R}$ produces a well-defined [linear map](/page/Linear%20Map) $\Phi^k$ on the cohomology [tensor product](/page/Tensor%20Product). Naturality in $M$ and $N$ — meaning compatibility with pullback along smooth maps $M' \to M$, $N' \to N$ — is the statement that pullback commutes with wedge product, which is true on the nose at the form level.[/guided]

[step:Set up the induction on the size of a finite good cover of $M$]Let $\mathcal{U} = \{U_1, \dots, U_p\}$ be a finite good cover of $M$. We prove that $\Phi^k$ is an isomorphism for every $k \in \mathbb{N}_0$ by induction on $p$. **Base case ($p = 1$).** Then $M$ is diffeomorphic to $\mathbb{R}^n$, where $n = \dim M$. In particular $M$ is smoothly contractible to a point $* \in M$. The constant map $c : M \to *$ and the inclusion $\iota_* : * \hookrightarrow M$ are smooth homotopy inverses. The product $M \times N$ deformation retracts smoothly onto $\{*\} \times N \cong N$ via $H : M \times N \times [0,1] \to M \times N$, $H(x, y, t) = (H_M(x, t), y)$, where $H_M$ is a smooth homotopy contracting $M$ to $*$. By [homotopy invariance of de Rham cohomology](/theorems/???), the pullback $\pi_N^*$ induces an isomorphism $H^j_{\mathrm{dR}}(N) \xrightarrow{\cong} H^j_{\mathrm{dR}}(M \times N)$. On the cohomology of $M$, the [Poincaré Lemma](/theorems/???) gives \begin{align*} H^i_{\mathrm{dR}}(M) = \begin{cases} \mathbb{R} \cdot [1_M], & i = 0, \\ 0, & i \ge 1, \end{cases} \end{align*} where $1_M \in \Omega^0(M)$ is the constant function with value $1$. Therefore \begin{align*} \bigoplus_{i+j=k} H^i_{\mathrm{dR}}(M) \otimes_{\mathbb{R}} H^j_{\mathrm{dR}}(N) \;=\; \mathbb{R} \cdot [1_M] \otimes_{\mathbb{R}} H^k_{\mathrm{dR}}(N), \end{align*} and $\Phi^k$ sends $[1_M] \otimes [\eta] \mapsto [\pi_M^* 1_M \wedge \pi_N^* \eta] = [\pi_N^* \eta]$. Since $\pi_N^*$ is an isomorphism on $H^k$ by the previous paragraph and the natural map $\mathbb{R} \otimes_{\mathbb{R}} V \to V$ is an isomorphism for every $\mathbb{R}$-[vector space](/page/Vector%20Space) $V$, $\Phi^k$ is an isomorphism in the base case. **Inductive hypothesis.** Suppose the theorem holds whenever $M$ admits a finite good cover of size $\le p - 1$.[/step]

[guided]The proof scheme — induction on the cardinality of a finite good cover — is the universal Bott–Tu tactic for de-Rham–theoretic statements. The point is that "good" intersections are diffeomorphic to $\mathbb{R}^n$, so the smallest pieces of the cover already have the cohomology of a point. The induction lets us bootstrap from those simple pieces by combining them through Mayer–Vietoris. For the base case the geometry is: $M \cong \mathbb{R}^n$ is contractible, so $M \times N$ retracts onto $N$. By the Poincaré Lemma the only surviving cohomology of $M$ is in degree $0$, namely the constant functions, and the right-hand side of Künneth collapses to $\mathbb{R} \otimes H^k(N) \cong H^k(N)$. The map $\Phi^k$ sends the canonical generator $[1_M] \otimes [\eta]$ to $[\pi_N^* \eta]$, which is exactly the homotopy-invariance isomorphism $H^k(N) \to H^k(M \times N)$. So $\Phi^k$ matches the identification we already had. Where does the explicit deformation retraction $H$ get used? It guarantees that $\pi_N^*$ — pullback along the projection $\pi_N : M \times N \to N$ — is an isomorphism on cohomology. The retraction $r : M \times N \to N$, $r(x, y) = y$, is left-inverse to $\iota : N \to M \times N$, $\iota(y) = (*, y)$, and the homotopy $H$ exhibits $\iota \circ r \simeq \mathrm{id}_{M \times N}$. Homotopy invariance then gives $r^* = \pi_N^*$ inducing the inverse of $\iota^*$ on cohomology.[/guided]

[step:Decompose $M$ via the good cover and verify the pieces have smaller good covers]For the inductive step, suppose $\mathcal{U} = \{U_1, \dots, U_p\}$ is a finite good cover of $M$ with $p \ge 2$. Set \begin{align*} U := U_1 \cup \cdots \cup U_{p-1}, \qquad V := U_p. \end{align*} Then $M = U \cup V$ is an open cover of $M$. - $\{U_1, \dots, U_{p-1}\}$ is a good cover of $U$ of size $p - 1$. - $\{V\}$ is a good cover of $V$ of size $1$ (since $V = U_p$ is diffeomorphic to $\mathbb{R}^n$). - The collection $\{U_1 \cap U_p, \dots, U_{p-1} \cap U_p\}$ is a good cover of $U \cap V$ of size $p - 1$: each $U_i \cap U_p$ is a nonempty intersection from $\mathcal{U}$ and hence diffeomorphic to $\mathbb{R}^n$ (or empty, in which case omit it), and finite intersections within this family are also intersections of members of $\mathcal{U}$, hence diffeomorphic to $\mathbb{R}^n$ or empty. By the inductive hypothesis, the cross product map $\Phi^k$ is an isomorphism for each of the manifolds $U$, $V$, $U \cap V$ in place of $M$.[/step]

[guided]The clever move here is the asymmetric split: rather than dividing the cover into two halves, we peel off a single [open set](/page/Open%20Set) $V = U_p$ and lump the rest into $U$. This is what makes the induction work, because the **intersection** $U \cap V$ inherits a good cover of size $p - 1$ — not $\binom{p}{2}$, as a symmetric split would force. Why does $\{U_i \cap U_p\}_{i=1}^{p-1}$ count as a good cover of $U \cap V$? A good cover requires every finite nonempty intersection to be diffeomorphic to $\mathbb{R}^n$. A finite intersection inside this family looks like $U_{i_1} \cap \cdots \cap U_{i_r} \cap U_p$ for some indices $i_1, \dots, i_r \in \{1, \dots, p-1\}$ — which is itself a finite intersection from the original good cover $\mathcal{U}$, hence either diffeomorphic to $\mathbb{R}^n$ or empty. So good-cover-ness is inherited. The size count is $p - 1$, strictly less than $p$, so the inductive hypothesis applies to each of $U$, $V$, $U \cap V$.[/guided]

[step:Build the Mayer–Vietoris ladder relating the cohomology of $M$ and $M \times N$]The cover $M = U \cup V$ induces, via the [Mayer–Vietoris Theorem](/theorems/1931), the long exact sequence \begin{align*} \cdots \to H^{i-1}_{\mathrm{dR}}(U \cap V) \xrightarrow{\delta_M} H^i_{\mathrm{dR}}(M) \to H^i_{\mathrm{dR}}(U) \oplus H^i_{\mathrm{dR}}(V) \to H^i_{\mathrm{dR}}(U \cap V) \xrightarrow{\delta_M} H^{i+1}_{\mathrm{dR}}(M) \to \cdots \end{align*} where the connecting map $\delta_M$ is the Mayer–Vietoris coboundary and the unmarked arrows are induced by inclusions $U \hookrightarrow M$, $V \hookrightarrow M$, $U \cap V \hookrightarrow U$, $U \cap V \hookrightarrow V$. The product cover $M \times N = (U \times N) \cup (V \times N)$ satisfies $(U \times N) \cap (V \times N) = (U \cap V) \times N$, and $\{U \times N, V \times N\}$ is again an open cover of $M \times N$. Mayer–Vietoris applied to this cover yields a second long exact sequence in $H^\bullet_{\mathrm{dR}}(M \times N)$, with connecting map $\delta_{M \times N}$. Tensor the first long exact sequence on the right with $H^j_{\mathrm{dR}}(N)$ and sum over $i + j = k$. Because $H^j_{\mathrm{dR}}(N)$ is an $\mathbb{R}$-[vector space](/page/Vector%20Space) and $\mathbb{R}$ is a field, the functor $- \otimes_{\mathbb{R}} H^j_{\mathrm{dR}}(N)$ is exact (every $\mathbb{R}$-module is free, hence flat); the direct sum over $i + j = k$ of exact sequences is exact. The result is the upper row of the following diagram, with the lower row given by Mayer–Vietoris for $M \times N$: \begin{align*} \begin{array}{ccccccc} \bigoplus_{i+j=k} H^{i-1}(U \cap V) \otimes H^j(N) & \to & \bigoplus_{i+j=k} H^i(M) \otimes H^j(N) & \to & \bigoplus_{i+j=k}\!\!\!\big(H^i(U) \oplus H^i(V)\big) \otimes H^j(N) & \to & \bigoplus_{i+j=k} H^i(U \cap V) \otimes H^j(N) \\[4pt] \downarrow \Phi^{k-1}_{U \cap V} & & \downarrow \Phi^k_M & & \downarrow \Phi^k_U \oplus \Phi^k_V & & \downarrow \Phi^k_{U \cap V} \\[4pt] H^{k-1}_{\mathrm{dR}}((U \cap V) \times N) & \to & H^k_{\mathrm{dR}}(M \times N) & \to & H^k_{\mathrm{dR}}(U \times N) \oplus H^k_{\mathrm{dR}}(V \times N) & \to & H^k_{\mathrm{dR}}((U \cap V) \times N) \end{array} \end{align*} Here we have written $H^i = H^i_{\mathrm{dR}}$ throughout, the subscripts on $\Phi$ indicate the manifold playing the role of "$M$" in the cross product, and the rows extend indefinitely in both directions.[/step]

[guided]We first write down the Mayer–Vietoris sequence for the open cover $M = U \cup V$. Let $\iota_U : U \hookrightarrow M$, $\iota_V : V \hookrightarrow M$, $\iota_{U \cap V,U} : U \cap V \hookrightarrow U$, and $\iota_{U \cap V,V} : U \cap V \hookrightarrow V$ denote the inclusion maps. The [Mayer–Vietoris Theorem](/theorems/2238) applies to this open cover and gives the long exact sequence \begin{align*} \cdots \to H^{i-1}_{\mathrm{dR}}(U \cap V) \xrightarrow{\delta_M} H^i_{\mathrm{dR}}(M) \to H^i_{\mathrm{dR}}(U) \oplus H^i_{\mathrm{dR}}(V) \to H^i_{\mathrm{dR}}(U \cap V) \xrightarrow{\delta_M} H^{i+1}_{\mathrm{dR}}(M) \to \cdots . \end{align*} The unmarked arrows are the pullback maps induced by the inclusions just named, and $\delta_M$ is the Mayer–Vietoris connecting homomorphism. Now pass to the product cover. Since products distribute over intersections, we have \begin{align*} (U \times N) \cap (V \times N) = (U \cap V) \times N. \end{align*} Thus \begin{align*} M \times N = (U \times N) \cup (V \times N) \end{align*} is an open cover. Applying the [Mayer–Vietoris Theorem](/theorems/2238) to this cover gives a second long exact sequence \begin{align*} \cdots \to H^{k-1}_{\mathrm{dR}}((U \cap V) \times N) \xrightarrow{\delta_{M \times N}} H^k_{\mathrm{dR}}(M \times N) \to H^k_{\mathrm{dR}}(U \times N) \oplus H^k_{\mathrm{dR}}(V \times N) \to H^k_{\mathrm{dR}}((U \cap V) \times N) \xrightarrow{\delta_{M \times N}} H^{k+1}_{\mathrm{dR}}(M \times N) \to \cdots . \end{align*} Why do we tensor the first sequence with $H^j_{\mathrm{dR}}(N)$ and then sum over $i+j=k$? The target Künneth object in total degree $k$ is \begin{align*} \bigoplus_{i+j=k} H^i_{\mathrm{dR}}(M) \otimes_{\mathbb{R}} H^j_{\mathrm{dR}}(N), \end{align*} so each entry in the Mayer–Vietoris sequence for $M$ must be converted into this graded tensor form. For each fixed $j$, the functor $- \otimes_{\mathbb{R}} H^j_{\mathrm{dR}}(N)$ is exact because $\mathbb{R}$ is a field and every $\mathbb{R}$-[vector space](/page/Vector%20Space) is flat. Finite direct sums of exact sequences are exact, so summing the tensorized sequences over $i+j=k$ preserves exactness. The resulting commutative ladder has upper row \begin{align*} \begin{array}{ccccccc} \bigoplus_{i+j=k} H^{i-1}(U \cap V) \otimes H^j(N) & \to & \bigoplus_{i+j=k} H^i(M) \otimes H^j(N) & \to & \bigoplus_{i+j=k}\!\!\!\big(H^i(U) \oplus H^i(V)\big) \otimes H^j(N) & \to & \bigoplus_{i+j=k} H^i(U \cap V) \otimes H^j(N) \\ \downarrow \Phi^{k-1}_{U \cap V} & & \downarrow \Phi^k_M & & \downarrow \Phi^k_U \oplus \Phi^k_V & & \downarrow \Phi^k_{U \cap V} \\ H^{k-1}_{\mathrm{dR}}((U \cap V) \times N) & \to & H^k_{\mathrm{dR}}(M \times N) & \to & H^k_{\mathrm{dR}}(U \times N) \oplus H^k_{\mathrm{dR}}(V \times N) & \to & H^k_{\mathrm{dR}}((U \cap V) \times N). \end{array} \end{align*} Here $H^a(X)$ abbreviates $H^a_{\mathrm{dR}}(X)$ only inside the displayed diagram, and every vertical arrow is the cross product map already defined for the indicated first factor. This diagram is the exact setup needed for the [five lemma](/theorems/1938): the upper row is the tensorized Mayer–Vietoris row for $M$, the lower row is the Mayer–Vietoris row for $M \times N$, and the vertical maps compare them by the cross product.[/guided]

[step:Verify that the Mayer–Vietoris ladder commutes]There are three types of squares to check. **Squares involving only restriction maps.** For a smooth map $f : X' \to X$, pullback satisfies $f^* (\alpha \wedge \beta) = f^* \alpha \wedge f^* \beta$. Applied to the inclusion $\iota_U : U \hookrightarrow M$ and the induced map $\iota_U \times \mathrm{id}_N : U \times N \to M \times N$, we have, for $\omega \in \Omega^i(M)$, $\eta \in \Omega^j(N)$: \begin{align*} (\iota_U \times \mathrm{id}_N)^* (\pi_M^* \omega \wedge \pi_N^* \eta) &= (\iota_U \times \mathrm{id}_N)^* \pi_M^* \omega \wedge (\iota_U \times \mathrm{id}_N)^* \pi_N^* \eta \\ &= \pi_U^* (\iota_U^* \omega) \wedge \pi_N^* \eta, \end{align*} using $\pi_M \circ (\iota_U \times \mathrm{id}_N) = \iota_U \circ \pi_U$ and $\pi_N \circ (\iota_U \times \mathrm{id}_N) = \pi_N$. This is the identity $\Phi^k_U \circ (\iota_U^* \otimes \mathrm{id}) = (\iota_U \times \mathrm{id}_N)^* \circ \Phi^k_M$ at the form level, which descends to cohomology. The same identity holds for $V$ and for the inclusion $U \cap V \hookrightarrow U$ (and into $V$). **Square involving the connecting homomorphism.** Let $\{\rho_U, \rho_V\}$ be a smooth [partition of unity](/page/Partition%20of%20Unity) on $M$ subordinate to $\{U, V\}$, with $\mathrm{supp}\,\rho_V \subseteq V$ and $\rho_U + \rho_V = 1$. The Mayer–Vietoris coboundary $\delta_M : H^i(U \cap V) \to H^{i+1}(M)$ is defined as follows: for a closed form $\sigma \in \Omega^i(U \cap V)$, the form $\rho_V \sigma$ extends by zero to a smooth form on $U$, and $-\rho_U \sigma$ extends by zero to a smooth form on $V$; these agree with $\sigma$ on $U \cap V$ up to the coboundary contribution, and $\delta_M [\sigma] := [d(\rho_V \sigma)] = [-d(\rho_U \sigma)]$ as a class on $M$ (the form $d(\rho_V \sigma)$ has support in $U \cap V$ and extends by zero to all of $M$, where it is closed because $d^2 = 0$ and $\sigma$ is closed). Pull back $\rho_U$ and $\rho_V$ along $\pi_M : M \times N \to M$. Then $\{\pi_M^* \rho_U, \pi_M^* \rho_V\}$ is a smooth [partition of unity](/page/Partition%20of%20Unity) on $M \times N$ subordinate to $\{U \times N, V \times N\}$, since \begin{align*} \pi_M^* \rho_U + \pi_M^* \rho_V = \pi_M^*(\rho_U + \rho_V) = \pi_M^* 1 = 1 \in C^\infty(M \times N). \end{align*} The coboundary $\delta_{M \times N}$ for the cover $\{U \times N, V \times N\}$ is constructed using exactly this [partition of unity](/page/Partition%20of%20Unity). Now compute, for $\sigma \in \Omega^i(U \cap V)$ closed and $\eta \in \Omega^j(N)$ closed: \begin{align*} \delta_{M \times N}\bigl(\Phi^{i+j}_{U \cap V}([\sigma] \otimes [\eta])\bigr) &= \delta_{M \times N}[\pi_{U \cap V}^* \sigma \wedge \pi_N^* \eta] \\ &= [d(\pi_M^* \rho_V \cdot \pi_{U \cap V}^* \sigma \wedge \pi_N^* \eta)] \\ &= [d(\pi_M^*(\rho_V \sigma)) \wedge \pi_N^* \eta] \\ &= [\pi_M^* d(\rho_V \sigma) \wedge \pi_N^* \eta] \\ &= \Phi^{i+j+1}_M\bigl([d(\rho_V \sigma)] \otimes [\eta]\bigr) \\ &= \Phi^{i+j+1}_M\bigl(\delta_M[\sigma] \otimes [\eta]\bigr). \end{align*} The identity $\pi_M^* \rho_V \cdot \pi_{U \cap V}^* \sigma = \pi_M^*(\rho_V \sigma)$ on $(U \cap V) \times N$ used in the second equality holds because the restriction of $\pi_M$ to $(U \cap V) \times N$ factors as $(U \cap V) \times N \xrightarrow{\pi_{U \cap V}} U \cap V \hookrightarrow M$, so $\pi_M^* \rho_V$ and $\pi_{U \cap V}^*(\rho_V|_{U \cap V})$ agree as functions on $(U \cap V) \times N$, and pullback is multiplicative on products of forms. Here the notation $\pi_M^*(\rho_V \sigma)$ means the pullback, to $(U \cap V) \times N$ and then extended by zero in the Mayer–Vietoris construction, of the smooth form $\rho_V\sigma$ on $U \cap V$; we are not extending $\sigma$ itself to $M$. We also used that $\pi_N^*\eta$ is closed and that pullback commutes with $d$. Summing over $i+j=k$ shows the connecting square commutes. In the abstract [tensor product](/page/Tensor%20Product) of cochain complexes a Koszul sign can appear when the differential passes across a degree-$j$ factor from $N$; in this proof the cross product is defined concretely by $[\sigma]\otimes[\eta]\mapsto[\pi^*\sigma\wedge\pi^*\eta]$, and $\eta$ is closed, so no additional sign appears in the displayed connecting-map computation.[/step]

[guided]A commutative ladder is the input to the [five lemma](/theorems/1938), so we verify the commutation at the level of representative differential forms. First consider a square involving only restriction maps. Let $\iota_U : U \hookrightarrow M$ denote the inclusion and let $\iota_U \times \mathrm{id}_N : U \times N \to M \times N$ be the induced product inclusion. The projection maps satisfy \begin{align*} \pi_M \circ (\iota_U \times \mathrm{id}_N) = \iota_U \circ \pi_U, \qquad \pi_N \circ (\iota_U \times \mathrm{id}_N) = \pi_N. \end{align*} For $\omega \in \Omega^i(M)$ and $\eta \in \Omega^j(N)$, functoriality of pullback and compatibility of pullback with wedge product give \begin{align*} (\iota_U \times \mathrm{id}_N)^* (\pi_M^* \omega \wedge \pi_N^* \eta) &= (\iota_U \times \mathrm{id}_N)^* \pi_M^* \omega \wedge (\iota_U \times \mathrm{id}_N)^* \pi_N^* \eta \\ &= \pi_U^* (\iota_U^* \omega) \wedge \pi_N^* \eta. \end{align*} This is exactly the identity \begin{align*} \Phi^k_U \circ (\iota_U^* \otimes \mathrm{id}) = (\iota_U \times \mathrm{id}_N)^* \circ \Phi^k_M \end{align*} on cohomology classes. The same calculation, with the inclusion name changed, proves the restriction squares for $V$ and for $U \cap V \hookrightarrow U$ and $U \cap V \hookrightarrow V$. It remains to check the square involving the connecting homomorphism. Choose a smooth [partition of unity](/page/Partition%20of%20Unity) $\{\rho_U,\rho_V\}$ on $M$ subordinate to $\{U,V\}$, with $\operatorname{supp}\rho_V \subseteq V$ and \begin{align*} \rho_U + \rho_V = 1. \end{align*} For a closed form $\sigma \in \Omega^i(U \cap V)$, the Mayer–Vietoris connecting homomorphism is represented by \begin{align*} \delta_M[\sigma] = [d(\rho_V\sigma)] = [-d(\rho_U\sigma)], \end{align*} where $\rho_V\sigma$ is regarded on $U \cap V$ and then extended by zero according to the Mayer–Vietoris construction. Pull the [partition of unity](/page/Partition%20of%20Unity) back along $\pi_M : M \times N \to M$. Then $\{\pi_M^*\rho_U,\pi_M^*\rho_V\}$ is a smooth [partition of unity](/page/Partition%20of%20Unity) subordinate to $\{U \times N,V \times N\}$, since \begin{align*} \pi_M^*\rho_U + \pi_M^*\rho_V = \pi_M^*(\rho_U+\rho_V) = \pi_M^*1 = 1 \in C^\infty(M \times N). \end{align*} Now let $\eta \in \Omega^j(N)$ be closed. Using the displayed representative for the connecting homomorphism on the product cover, the closedness of $\eta$, and the identity $d\circ\pi_M^*=\pi_M^*\circ d$, we compute \begin{align*} \delta_{M \times N}\bigl(\Phi^{i+j}_{U \cap V}([\sigma]\otimes[\eta])\bigr) &= \delta_{M \times N}[\pi_{U \cap V}^*\sigma \wedge \pi_N^*\eta] \\ &= [d(\pi_M^*\rho_V \cdot \pi_{U \cap V}^*\sigma \wedge \pi_N^*\eta)] \\ &= [d(\pi_M^*(\rho_V\sigma)) \wedge \pi_N^*\eta] \\ &= [\pi_M^*d(\rho_V\sigma) \wedge \pi_N^*\eta] \\ &= \Phi^{i+j+1}_M([d(\rho_V\sigma)]\otimes[\eta]) \\ &= \Phi^{i+j+1}_M(\delta_M[\sigma]\otimes[\eta]). \end{align*} The second equality uses the identity $\pi_M^*\rho_V \cdot \pi_{U \cap V}^*\sigma = \pi_M^*(\rho_V\sigma)$ on $(U \cap V) \times N$: this holds because the restriction of $\pi_M$ to $(U \cap V) \times N$ factors through $U \cap V$, so $\pi_M^*\rho_V$ agrees on $(U \cap V) \times N$ with $\pi_{U \cap V}^*(\rho_V|_{U \cap V})$, and pullback distributes over products of forms. The expression $\pi_M^*(\rho_V\sigma)$ refers to the pullback of the form $\rho_V\sigma$ used in the Mayer–Vietoris construction; it does not require extending $\sigma$ itself to $M$. In the abstract [tensor product](/page/Tensor%20Product) of complexes a Koszul sign can arise when a differential crosses the degree-$j$ factor from $N$, but this concrete computation uses the cross product $[\sigma]\otimes[\eta]\mapsto[\pi^*\sigma\wedge\pi^*\eta]$ and $d_N\eta=0$, so no extra sign appears here. Therefore the connecting square commutes, and hence the whole Mayer–Vietoris ladder commutes.[/guided]

[step:Apply the five lemma to deduce the inductive step]The diagram from the previous two steps is a commutative ladder whose rows are long exact sequences. By the inductive hypothesis (Step 3) applied to the three manifolds $U$, $V$, $U \cap V$ — each of which admits a good cover of size at most $p - 1$ — the four vertical maps \begin{align*} \Phi^k_U, \quad \Phi^k_V, \quad \Phi^k_{U \cap V}, \quad \Phi^{k-1}_{U \cap V} \end{align*} are isomorphisms for every $k$. The fifth vertical, $\Phi^k_U \oplus \Phi^k_V$, is a direct sum of isomorphisms and therefore itself an isomorphism. Applying the [Five Lemma](/theorems/1938) to the segment \begin{align*} \begin{array}{ccccccccc} \cdot & \to & \cdot & \to & \bigoplus_{i+j=k} H^i(M) \otimes H^j(N) & \to & \cdot & \to & \cdot \\ \downarrow \cong & & \downarrow \cong & & \downarrow \Phi^k_M & & \downarrow \cong & & \downarrow \cong \\ \cdot & \to & \cdot & \to & H^k(M \times N) & \to & \cdot & \to & \cdot \end{array} \end{align*} (where the outer four vertical maps are the four isomorphisms above) forces $\Phi^k_M$ to be an isomorphism. This closes the induction: $\Phi^k$ is an isomorphism for $M$ admitting a finite good cover of size $p$.[/step]

[guided]The [five lemma](/theorems/1938) states: in a commutative ladder \begin{align*} \begin{array}{ccccccccc} A_1 & \to & A_2 & \to & A_3 & \to & A_4 & \to & A_5 \\ \downarrow f_1 & & \downarrow f_2 & & \downarrow f_3 & & \downarrow f_4 & & \downarrow f_5 \\ B_1 & \to & B_2 & \to & B_3 & \to & B_4 & \to & B_5 \end{array} \end{align*} with exact rows, if $f_1, f_2, f_4, f_5$ are isomorphisms then $f_3$ is too. We have arranged for $f_3 = \Phi^k_M$ and the surrounding four maps to be isomorphisms by induction. So $\Phi^k_M$ is an isomorphism. Why is $\Phi^k_U \oplus \Phi^k_V$ — a single map between direct sums — also an isomorphism? Because the direct sum of two isomorphisms is an isomorphism: bijectivity, linearity, and inverse all pass through direct sums. This completes the inductive step. We have shown that if $\Phi$ is an isomorphism whenever the first factor has a good cover of size $\le p - 1$, then $\Phi$ is an isomorphism whenever the first factor has a good cover of size $\le p$.[/guided]

[step:Conclude the proof by induction] By induction on $p$, the cross product map $\Phi^k$ is an isomorphism for every smooth manifold $M$ admitting a finite good cover and every smooth manifold $N$. Naturality was checked at the form level in Step 1 and is preserved by descent to cohomology. This establishes the natural isomorphism \begin{align*} \bigoplus_{i+j=k} H^i_{\mathrm{dR}}(M) \otimes_{\mathbb{R}} H^j_{\mathrm{dR}}(N) \;\xrightarrow{\;\cong\;}\; H^k_{\mathrm{dR}}(M \times N) \end{align*} for every $k \in \mathbb{N}_0$, completing the proof of the [Künneth Theorem](/theorems/2274) for de Rham cohomology. $\blacksquare$ [/step]