theorem Th32: :: GR_FREE0:31

for I being non empty set
for i being Element of I
for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G
for g, h being Element of (G . i) st g * h = 1_ (G . i) holds
ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q