theorem Th65: :: GR_FREE0:64

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) st len (nf s) = 1 holds
ex i being Element of I ex g being Element of (H . i) st
( g <> 1_ (H . i) & s = [*i,g*] )