theorem Th42: :: GR_FREE0:41

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I st I is trivial holds
for p being non empty FinSequence of FreeAtoms G ex g being Element of (G . i) st ReductionRel G reduces p,<*[i,g]*>