theorem Th59: :: GR_FREE0:58

for I being non empty set
for H being Group-like associative multMagma-Family of I
for p being FinSequence of FreeAtoms H
for s being Element of (FreeProduct H) st s = Class ((EqCl (ReductionRel H)),p) holds
nf s = nf (p,(ReductionRel H))