theorem Th33: :: GR_FREE0:32

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