:: deftheorem defines factorization GR_FREE0:def 10 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for s being Element of (FreeProduct H) holds factorization s = (uncurry (injection H)) * (nf s);