theorem Th45: :: GR_FREE0:44

for I being set
for H being Group-like associative multMagma-Family of I holds 1_ (FreeProduct H) = Class ((EqCl (ReductionRel H)),{})