theorem Th72: :: GR_FREE0:71

for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) holds Product (factorization s) = s