theorem Th22: :: GR_FREE0:21

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