The fundamental class of a product is the cross product of the fundamental classes

Since $M$ and $N$ are closed, $M\times N$ is a closed smooth $(m+n)$-manifold with the product smooth structure and empty boundary [F8], and the product orientation of [F2] is an $R$-orientation of it. By [F1] the fundamental class $[M\times N]$ is the unique class in $H_{m+n}(M\times N;R)$ whose restriction at each point is the local generator attached to the ray of the product orientation, and [F5] makes the class $[M]\times [N]$ well defined. It therefore suffices to prove that for every $(x,y)$ the restriction of $[M]\times [N]$ to $H_{m+n}(M\times N,M\times N\setminus \{(x,y)\};R)$ is the local generator attached to the tensor ray of ${\mu }_x$ and ${\nu }_y$.

Model computation. In ${\mathbb{R}}^m$ let $c$ be an affine $m$-simplex whose image contains $0$ in its interior and whose affine parametrization is orientation-preserving, and in ${\mathbb{R}}^n$ let $d$ be such an $n$-simplex; write ${\rho }_m,{\rho }_n,{\rho }_{m+n}$ for the positive local generators of the standard orientations. For $m,n>0$ choose the two simplices so that $(0,0)$ avoids the internal faces of their finite shuffle triangulation; this is possible by varying the two interior barycentric coordinates to avoid finitely many proper affine hyperplanes. The boundaries of $c$ and $d$ avoid the origin, so $c$ and $d$ are relative cycles representing ${\rho }_m$ and ${\rho }_n$, and by [F3] the boundary $\mathrm{\partial }(c\times d)=\mathrm{\partial }c\times d+(-1{)}^{m}c\times \mathrm{\partial }d$ lies in $C(({\mathbb{R}}^m\setminus \{0\})\times {\mathbb{R}}^n)+C({\mathbb{R}}^m\times ({\mathbb{R}}^n\setminus \{0\}))\subseteq C({\mathbb{R}}^{m+n}\setminus \{0\})$, so $c\times d$ is a relative cycle for the pair $({\mathbb{R}}^{m+n},{\mathbb{R}}^{m+n}\setminus \{0\})$. Its shuffle expansion is the sum of the terms $\mathrm{sgn}(\theta )(c\times d)\circ {\lambda }_{\theta }$ over all $(m,n)$-shuffles $\theta$ [F3]: the vertices of ${\lambda }_{\theta }$ are the successive vertices of the lattice path of $\theta$, so consecutive differences of its edge columns give the ordered coordinate increments of the path, with determinant $\mathrm{sgn}(\theta )$; subtracting successive columns does not change the determinant, so the coefficient $\mathrm{sgn}(\theta )$ makes every term positively oriented, and the images of these simplices have pairwise disjoint interiors and cover the product of the two simplex images, the standard lattice-path triangulation of a product simplex. Exactly one shuffle simplex contains the origin in its interior, and all other shuffle simplices avoid it. Its oriented class is therefore the positive local generator; equivalently $c\times d$ covers a neighbourhood of the origin exactly once, positively oriented, so by the chart convention of [F1] its class is the positive generator ${\rho }_{m+n}$ of the local group of ${\mathbb{R}}^{m+n}$ at the origin; that is, ${\rho }_m\times {\rho }_n={\rho }_{m+n}$ for the standard, hence product, orientation.

For relative cycles $c\in C_m(M,M\setminus \{x\};R)$ and $d\in C_n(N,N\setminus \{y\};R)$, the boundary formula makes $c\times d$ a relative cycle off $(x,y)$: its boundary terms are supported in $(M\setminus \{x\})\times N$ or $M\times (N\setminus \{y\})$. Changing $c$ by $\mathrm{\partial }e$ changes the product by $\mathrm{\partial }(e\times d)-(-1{)}^{m+1}e\times \mathrm{\partial }d$, a relative boundary because the second term misses $y$; changing $d$ by $\mathrm{\partial }f$ has the analogous effect, with the remaining term missing $x$. Chains already supported off $x$ or $y$ also produce chains off $(x,y)$. Thus the cross product descends to the local relative groups, and quotienting absolute cycles shows that the restriction of $[M]\times [N]$ is the cross product of their local restrictions.

First suppose $m,n>0$. Choose charts $\phi :(U,x)\to ({\mathbb{R}}^m,0)$ and $\psi :(V,y)\to ({\mathbb{R}}^n,0)$, replacing either chart by its composition with a reflection of the corresponding Euclidean space if necessary, in the integral case so that $d{\phi }_x$ and $d{\psi }_y$ carry the orientation rays of $M$ at $x$ and of $N$ at $y$ to the standard rays. Over ${\mathbb{F}}_2$ take any charts, since either sign gives the canonical local generator. In the integral case this also makes $d(\phi \times \psi {)}_{(x,y)}=d{\phi }_x\oplus d{\psi }_y$ carry the product ray to the standard ray of ${\mathbb{R}}^{m+n}={\mathbb{R}}^m\times {\mathbb{R}}^n$ [F2]. The chart maps induce isomorphisms of the local pairs and, by naturality [F4, F5], carry the relative cross product of step 1.3 to the relative cross product in the models, while by the chart convention of [F1] the local generators ${\mu }_x$, ${\nu }_y$ correspond to the positive generators ${\rho }_m$, ${\rho }_n$ of the model local groups and the product-orientation generator to ${\rho }_{m+n}$. The required pointwise identity at $(x,y)$ is therefore exactly the model identity ${\rho }_m\times {\rho }_n={\rho }_{m+n}$ proved in step 1.2. If a factor is zero-dimensional, its local fundamental class is its supplied sign times the point cycle (or the unique nonzero point cycle over ${\mathbb{F}}_2$). The point-factor shuffle has a single term; bilinearity carries that sign into the product local generator, so no nonexistent orientation-reversing zero-dimensional chart is needed.

Steps 1.2, 1.3 and 2.1 show that the restriction of $[M]\times [N]$ at every point $(x,y)$ of $M\times N$ is the local generator of the product orientation, so the characterizing property of the fundamental class [F1] gives $[M\times N]=[M]\times [N]$ in $H_{m+n}(M\times N;R)$; this is the integral identity for $R=\mathbb{Z}$. For $R={\mathbb{F}}_2$ the same shuffle formula has all signs equal to $1$, the local groups are ${\mathbb{F}}_2$ with the canonical orientation of [F7], and the computation of step 1.2 is unchanged, so the identity holds in $H_{m+n}(M\times N;{\mathbb{F}}_2)$ as well. For a disjoint union $M={⨆}_i{M}_i$ the fundamental class is the sum of the component fundamental classes and the cross product is bilinear [F1, F5], so applying the identity to each component pair gives $[M\times N]={\sum }_{i,j}[M_i\times N_j]=({\sum }_i[M_i])\times ({\sum }_j[N_j])=[M]\times [N]$; this is the asserted compatibility with the componentwise definition, and by [F6] the same reduction would already follow from checking one point in each connected component. If $M$ or $N$ is empty then $M\times N$ is empty and both sides are the zero class in the zero group; if $m=0$ or $n=0$ the corresponding shuffle set has one element of sign $1$ and the computation of step 1.2 covers the point factors.