let I be non empty set ; :: thesis: 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 ")] ) )
let H be Group-like associative multMagma-Family of I; :: thesis: 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 ")] ) )
let p be FinSequence of FreeAtoms H; :: thesis: 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 ")] ) )
consider q being FinSequence of FreeAtoms H such that
A1: len p = len q and
A2: for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
ex h being Element of (H . i) st
( g * h = 1_ (H . i) & (Rev q) . k = [i,h] ) by Th21;
take q ; :: thesis: ( 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 ")] ) )
thus len p = len q by A1; :: thesis: 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 ")]
let k be Nat; :: thesis: for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")]
let i be Element of I; :: thesis: for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")]
let g be Element of (H . i); :: thesis: ( p . k = [i,g] implies (Rev q) . k = [i,(g ")] )
assume p . k = [i,g] ; :: thesis: (Rev q) . k = [i,(g ")]
then consider h being Element of (H . i) such that
A3: ( g * h = 1_ (H . i) & (Rev q) . k = [i,h] ) by A2;
thus (Rev q) . k = [i,(g ")] by A3, GROUP_1:12; :: thesis: verum