theorem Th63: :: GR_FREE0:62

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) = 0 holds
s = 1_ (FreeProduct H)