The natural PID Kunneth sequence is exact

Write $u:H_{n}X\to H_{n}T$ and $v:H_{n}T\to H_{n}Y$ for the maps of [F1], with $T=C\otimes D$. Its LES gives $\ker u=\mathrm{im}{\mathrm{\partial }}_{n+1}$, $\ker v=\mathrm{im}u$, and $\mathrm{im}v=\ker {\mathrm{\partial }}_n$. Therefore $\bar{u}:\mathrm{coker}{\mathrm{\partial }}_{n+1}\to H_{n}T$, $[x]\mapsto u(x)$, is well defined and injective: $u(x)=0$ exactly when $x\in \mathrm{im}{\mathrm{\partial }}_{n+1}$.

Let $f:C\to C^{\mathrm{\prime }}$ and $g:D\to D^{\mathrm{\prime }}$ be chain maps between complexes satisfying the hypotheses. The relation $d_{C^{\mathrm{\prime }}}f=f{d}_C$ sends cycles to cycles and boundaries to boundaries, and gives ${\rho }^{\mathrm{\prime }}f=A(f)\rho$, where $A(f{)}_p$ is $f_{p-1}$ restricted to $B_{p-1}C$. Thus $(Z(f)\otimes g,f\otimes g,A(f)\otimes g)$ is a morphism of the canonical short exact tensor sequences. By [F4] it commutes with $u,v,\mathrm{\partial }$, hence with their induced kernel/cokernel maps.

The corestriction $\bar{v}:H_{n}T\to \ker {\mathrm{\partial }}_n$ is onto and has kernel $\mathrm{im}\bar{u}$. Thus $0\to \mathrm{coker}{\mathrm{\partial }}_{n+1}\stackrel{\bar{u}}{\to }{H}_{n}T\stackrel{\bar{v}}{\to }\ker {\mathrm{\partial }}_n\to 0$ is exact. Under the explicit identifications in [F1], $\bar{u}$ is precisely ${\alpha }_n$ of [F2], and $\bar{v}$ is precisely ${\beta }_n$ of [F3]. This proves all three exactness assertions for the maps in the statement.

The cokernel identification commutes with these maps since $z\otimes [w]$ goes to $f(z)\otimes [g(w)]$ and then to $[f(z)]\otimes [g(w)]$. On a kernel summand, the maps $B_{r}C\to B_r{C}^{\mathrm{\prime }}$ and $Z_{r}C\to Z_r{C}^{\mathrm{\prime }}$ form a map of the actual length-one resolutions lifting $H_{r}f$. Tensoring with $H_{q}g$ induces the Tor map used by the natural quotient [F3]. Hence step 1.2 gives both naturality squares for the displayed sequence. Equivalently the first square follows by evaluating [F2] on $[z]\otimes [w]$. No selected sections enter $\rho$, these resolution maps, or the two final arrows.

At $n=0$ the Tor sum is empty, so exactness makes ${\alpha }_0:H_{0}C\otimes H_{0}D\to H_{0}T$ an isomorphism. At $n=1$ the right term is ${\mathrm{Tor}}_1(H_{0}C,H_{0}D)$. If one complex is zero, $X,T,Y$ and both end terms are zero, so the same proof gives the zero exact sequence. There is no upper endpoint: for each $n$ only finitely many pairs $p+q=n$ occur, regardless of the ranks.