theorem Th21: :: GR_FREE0:20

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