theorem Th70: :: GR_FREE0:69

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s, t being Element of (FreeProduct H) st ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 holds
factorization (s * t) = (factorization s) ^ (factorization t)