theorem Th66: :: GR_FREE0:65

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
nf (s * t) = (nf s) ^ (nf t)