theorem Th29: :: GR_FREE0:28

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I holds [<*[i,(1_ (G . i))]*>,{}] in ReductionRel G