${\pi }_1(X\times Y,(x_0,y_0))\cong {\pi }_1(X,x_0)\times {\pi }_1(Y,y_0)$

Projection sends a loop in $X\times Y$ to one loop in each factor. If two product loops are path-homotopic relative to endpoints, composing the homotopy with either projection gives a path homotopy of the coordinate loops by [F4]. Thus the displayed rule $\mathrm{\Theta }$ is well defined.

Conversely, [F1] makes $s\mapsto (\alpha (s),\beta (s))$ a continuous based loop. Pairing two endpoint-fixed homotopies gives a product homotopy by the same characteristic property, so the resulting class depends only on $[\alpha ]$ and $[\beta ]$. This defines a function $\mathrm{\Xi }$ from the direct product to ${\pi }_1(X\times Y,(x_0,y_0))$.

Projections commute with concatenation, so [F2] and [F3] show that $\mathrm{\Theta }$ is a group homomorphism.

Coordinatewise concatenation shows that $\mathrm{\Xi }$ is a homomorphism. By construction $\mathrm{\Theta }\mathrm{\Xi }([\alpha ],[\beta ])=([\alpha ],[\beta ])$, and uniqueness of a map with given coordinates in [F1] gives $\mathrm{\Xi }\mathrm{\Theta }[\gamma ]=[\gamma ]$. Hence $\mathrm{\Theta }$ and $\mathrm{\Xi }$ are inverse group isomorphisms.

Let $f:(X,x_0)\to (X^{\mathrm{\prime }},x_0^{\mathrm{\prime }})$ and $g:(Y,y_0)\to (Y^{\mathrm{\prime }},y_0^{\mathrm{\prime }})$ be pointed continuous maps. By [F1], their product $f\times g$ is pointed and continuous. Composition with any pointed continuous map preserves endpoint-fixed homotopies and commutes with loop concatenation, so [F2], [F4], and [F5] make all three induced maps in the naturality square well-defined homomorphisms. For every product-loop class $[\gamma ]$, both $(f_{\ast }\times g_{\ast }){\mathrm{\Theta }}_{X,Y}[\gamma ]$ and ${\mathrm{\Theta }}_{X^{\mathrm{\prime }},Y^{\mathrm{\prime }}}(f\times g{)}_{\ast }[\gamma ]$ equal $([f\circ {\pi }_X\circ \gamma ],[g\circ {\pi }_Y\circ \gamma ])\mathrm{.}$ Thus the naturality square commutes for every pair $(f,g)$, so the displayed group isomorphism is natural.