let I be non empty set ; :: thesis: 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] ) ) )
let G be Group-like multMagma-Family of I; :: thesis: 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] ) ) )
let p be FinSequence of FreeAtoms G; :: thesis: 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] ) ) )
defpred S₁[ object , object ] means ex i being Element of I ex g, h being Element of (G . i) st
( p . $1 = [i,g] & g * h = 1_ (G . i) & $2 = [i,h] );

A1: now :: thesis: for k being Nat st k in Seg (len p) holds
ex z being Element of FreeAtoms G st S₁[k,z]

let k be Nat; :: thesis: ( k in Seg (len p) implies ex z being Element of FreeAtoms G st S₁[k,z] )
assume k in Seg (len p) ; :: thesis: ex z being Element of FreeAtoms G st S₁[k,z]
then k in dom p by FINSEQ_1:def 3;
then A2: p . k in rng p by FUNCT_1:3;
then consider i, g being object such that
A3: p . k = [i,g] by RELAT_1:def 1;
i in dom G by A2, A3, Th7;
then reconsider i = i as Element of I ;
reconsider g = g as Element of (G . i) by A2, A3, Th9;
consider e being Element of (G . i) such that
A4: for h0 being Element of (G . i) holds
( h0 * e = h0 & e * h0 = h0 & ex g0 being Element of (G . i) st
( h0 * g0 = e & g0 * h0 = e ) ) by GROUP_1:def 2;
A5: e = 1_ (G . i) by A4, GROUP_1:def 4;
consider h being Element of (G . i) such that
A6: ( g * h = e & h * g = e ) by A4;
reconsider z = [i,h] as Element of FreeAtoms G by Th9;
take z = z; :: thesis: S₁[k,z]
thus S₁[k,z] by A3, A5, A6; :: thesis: verum

end;

consider q9 being FinSequence of FreeAtoms G such that
A7: ( dom q9 = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S₁[k,q9 . k] ) ) from FINSEQ_1:sch 5(A1);
take Rev q9 ; :: thesis: ( len p = len (Rev q9) & ( 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 (Rev q9)) . k = [i,h] ) ) )
thus len p = len q9 by A7, FINSEQ_1:def 3
.= len (Rev q9) by FINSEQ_5:def 3 ; :: thesis: 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 (Rev q9)) . k = [i,h] )
let k be Nat; :: thesis: 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 (Rev q9)) . k = [i,h] )
let i be Element of I; :: thesis: 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 (Rev q9)) . k = [i,h] )
let g be Element of (G . i); :: thesis: ( p . k = [i,g] implies ex h being Element of (G . i) st
( g * h = 1_ (G . i) & (Rev (Rev q9)) . k = [i,h] ) )

per cases ( not k in Seg (len p) or k in Seg (len p) ) ;

suppose not k in Seg (len p) ; :: thesis: ( p . k = [i,g] implies ex h being Element of (G . i) st
( g * h = 1_ (G . i) & (Rev (Rev q9)) . k = [i,h] ) )

then not k in dom p by FINSEQ_1:def 3;
hence ( p . k = [i,g] implies ex h being Element of (G . i) st
( g * h = 1_ (G . i) & (Rev (Rev q9)) . k = [i,h] ) ) by FUNCT_1:def 2; :: thesis: verum

end;

suppose k in Seg (len p) ; :: thesis: ( p . k = [i,g] implies ex h being Element of (G . i) st
( g * h = 1_ (G . i) & (Rev (Rev q9)) . k = [i,h] ) )

then consider i0 being Element of I, g0, h being Element of (G . i0) such that
A8: ( p . k = [i0,g0] & g0 * h = 1_ (G . i0) & q9 . k = [i0,h] ) by A7;
assume p . k = [i,g] ; :: thesis: ex h being Element of (G . i) st
( g * h = 1_ (G . i) & (Rev (Rev q9)) . k = [i,h] )
then A9: ( i = i0 & g = g0 ) by A8, XTUPLE_0:1;
then reconsider h = h as Element of (G . i) ;
take h ; :: thesis: ( g * h = 1_ (G . i) & (Rev (Rev q9)) . k = [i,h] )
thus g * h = 1_ (G . i) by A8, A9; :: thesis: (Rev (Rev q9)) . k = [i,h]
thus (Rev (Rev q9)) . k = [i,h] by A8, A9; :: thesis: verum

end;

end;