Normal form theorem for free products

Given: The objects and hypotheses in the statement.

The reduced syllable words in $(G_i)_{i\in I}$ form a group under concatenation followed by seam reduction. The one-syllable maps $G_i\to W$ make this group a free product of the family. (Reduced syllable words form the free product of a family of groups).

For groups as in def-group, a syllable is a tagged pair $(i,g)$ with $i\in I$ and $g\in G_i\setminus\{e_i\}$. A reduced syllable word is a finite list of syllables, indexed by a natural length as in def-natural-numbers, in which adjacent tags differ. The empty list is allowed. At a concatenation seam, adjacent syllables from the same factor are multiplied and an identity result is deleted; this elementary reduction is repeated until the seam is reduced. (Reduced syllable words in a family of groups).

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).