Free groups on disjoint bases freely multiply to the free group on their union

Given: The objects and hypotheses in the statement.

A free group on a set $X$ is a group $F(X)$ together with a map $i:X\to F(X)$ such that, for every group $G$ and every function $u:X\to G$, there is a unique group homomorphism $\widehat u:F(X)\to G$ satisfying $\widehat u\circ i=u.$ The reduced-word construction supplies such a group; the construction and its universal property are established in thm-reduced-words-form-the-free-group. When no ambiguity arises, $x\in X$ is identified with its image $i(x)$. (Free group on a set of generators).

If $(F,i)$ and $(F',i')$ are free groups on the same set $X$, then there is a unique group isomorphism $\phi:F\to F'$ such that $\phi\circ i=i'.$ (Free groups on the same set are uniquely isomorphic compatibly with their generators).

For a family $(G_i)_{i\in I}$, a free product is a group $F$ with homomorphisms $\iota_i:G_i\to F$ in the sense of def-group-homomorphism, such that for every group $H$ and every family of homomorphisms $f_i:G_i\to H$, there is a unique homomorphism $f:F\to H$ satisfying $f\circ\iota_i=f_i$ for all $i$. It is denoted $\ast_{i\in I}G_i$. Injectivity of the maps $\iota_i$ is not part of this definition. (The free product of an arbitrary family of groups).

Any two free products of the same family are connected by a unique isomorphism commuting with every canonical factor map. (Free products are unique up to a unique factor-compatible isomorphism).