Normal form theorem for a free product (source code)

= Normal form theorem for a free product

Every element of a <free product> $G*H$ has a unique expression $u_1\cdots u_n$ in which each $u_i$ is a nonidentity element of one factor and adjacent syllables belong to different factors. The identity corresponds to the empty word.