let I be non empty set ; :: thesis: 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, {}
let G be Group-like multMagma-Family of I; :: thesis: 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, {}
defpred S₁[ FinSequence, FinSequence] means ( len $1 = len $2 & ( for k being Nat
for i being Element of I
for g, h being Element of (G . i) st $1 . k = [i,g] & g * h = 1_ (G . i) holds
(Rev $2) . k = [i,h] ) implies ReductionRel G reduces $1 ^ $2, {} );
defpred S₂[ Nat] means for p, q being FinSequence of FreeAtoms G st len p = $1 holds
S₁[p,q];
A1: S₂[ 0 ]

proof

let p, q be FinSequence of FreeAtoms G; :: thesis: ( len p = 0 implies S₁[p,q] )
assume ( len p = 0 & len p = len q ) ; :: thesis: ( ex k being Nat ex i being Element of I ex g, h being Element of (G . i) st
( p . k = [i,g] & g * h = 1_ (G . i) & not (Rev q) . k = [i,h] ) or ReductionRel G reduces p ^ q, {} )
then ( p = {} & q = {} ) ;
then p ^ q = {} by FINSEQ_1:34;
hence ( ex k being Nat ex i being Element of I ex g, h being Element of (G . i) st
( p . k = [i,g] & g * h = 1_ (G . i) & not (Rev q) . k = [i,h] ) or ReductionRel G reduces p ^ q, {} ) by REWRITE1:12; :: thesis: verum

end;

A2: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A3: S₂[n] ; :: thesis: S₂[n + 1]
let p, q be FinSequence of FreeAtoms G; :: thesis: ( len p = n + 1 implies S₁[p,q] )
assume A4: ( len p = n + 1 & len p = len q ) ; :: thesis: ( ex k being Nat ex i being Element of I ex g, h being Element of (G . i) st
( p . k = [i,g] & g * h = 1_ (G . i) & not (Rev q) . k = [i,h] ) or ReductionRel G reduces p ^ q, {} )
assume A5: 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] ; :: thesis: ReductionRel G reduces p ^ q, {}
consider p9 being FinSequence of FreeAtoms G, z1 being Element of FreeAtoms G such that
A6: p = p9 ^ <*z1*> by A4, FINSEQ_2:19;
len (Rev q) = n + 1 by A4, FINSEQ_5:def 3;
then consider q9 being FinSequence of FreeAtoms G, z2 being Element of FreeAtoms G such that
A7: Rev q = q9 ^ <*z2*> by FINSEQ_2:19;
( len p = (len p9) + 1 & len (Rev q) = (len q9) + 1 ) by A6, A7, FINSEQ_2:16;
then ( len p9 = n & len q = (len q9) + 1 ) by A4, FINSEQ_5:def 3;
then A8: ( len p9 = n & len q9 = n ) by A4;
then A9: len p9 = len (Rev q9) by FINSEQ_5:def 3;
A10: Rev (Rev q) = <*z2*> ^ (Rev q9) by A7, FINSEQ_5:63;
for k being Nat
for i being Element of I
for g, h being Element of (G . i) st p9 . k = [i,g] & g * h = 1_ (G . i) holds
(Rev (Rev q9)) . k = [i,h]

proof

let k be Nat; :: thesis: for i being Element of I
for g, h being Element of (G . i) st p9 . k = [i,g] & g * h = 1_ (G . i) holds
(Rev (Rev q9)) . k = [i,h]
let i be Element of I; :: thesis: for g, h being Element of (G . i) st p9 . k = [i,g] & g * h = 1_ (G . i) holds
(Rev (Rev q9)) . k = [i,h]
let g, h be Element of (G . i); :: thesis: ( p9 . k = [i,g] & g * h = 1_ (G . i) implies (Rev (Rev q9)) . k = [i,h] )
assume A11: ( p9 . k = [i,g] & g * h = 1_ (G . i) ) ; :: thesis: (Rev (Rev q9)) . k = [i,h]
then A12: k in dom p9 by FUNCT_1:def 2;
then p . k = [i,g] by A6, A11, FINSEQ_1:def 7;
then A13: (Rev q) . k = [i,h] by A5, A11;
A14: dom p9 = dom q9 by A8, FINSEQ_3:29
.= dom (Rev q9) by FINSEQ_5:57 ;
then A15: k in dom (Rev q9) by A12;
A16: len p9 = len (Rev q9) by A14, FINSEQ_3:29;
k in Seg (len p9) by A12, FINSEQ_1:def 3;
then ((len p9) - k) + 1 in Seg (len p9) by FINSEQ_5:2;
then A17: ((len (Rev q9)) - k) + 1 in dom (Rev q9) by A16, FINSEQ_1:def 3;
k in dom p by A6, A12, FINSEQ_1:26, TARSKI:def 3;
then k in Seg (len q) by A4, FINSEQ_1:def 3;
then ((len q) - k) + 1 in Seg (len q) by FINSEQ_5:2;
then A18: ((len (Rev q)) - k) + 1 in Seg (len q) by FINSEQ_5:def 3;
then reconsider m = ((len (Rev q)) - k) + 1 as Nat ;
m in dom q by A18, FINSEQ_1:def 3;
then m in dom (Rev q) by FINSEQ_5:57;
then A19: (Rev (Rev q)) . m = (Rev q) . (((len (Rev q)) - m) + 1) by FINSEQ_5:58
.= (Rev q) . k ;
thus (Rev (Rev q9)) . k = (Rev q9) . (((len (Rev q9)) - k) + 1) by A15, FINSEQ_5:58
.= (<*z2*> ^ (Rev q9)) . ((len <*z2*>) + (((len (Rev q9)) - k) + 1)) by A17, FINSEQ_1:def 7
.= q . ((((len <*z2*>) + (len (Rev q9))) - k) + 1) by A10
.= q . (((len q) - k) + 1) by A10, FINSEQ_1:22
.= [i,h] by A13, A19, FINSEQ_5:def 3 ; :: thesis: verum

end;

then A20: ReductionRel G reduces p9 ^ (Rev q9), {} by A3, A8, A9;
consider i, g being object such that
A21: z1 = [i,g] by RELAT_1:def 1;
i in dom G by A21, Th7;
then reconsider i = i as Element of I ;
reconsider g = g as Element of (G . i) by A21, Th9;
A22: p . (len p) = p . ((len p9) + 1) by A6, FINSEQ_2:16
.= [i,g] by A6, A21, FINSEQ_1:42 ;
consider e being Element of (G . i) such that
A23: for g9 being Element of (G . i) holds
( g9 * e = g9 & e * g9 = g9 & ex h being Element of (G . i) st
( g9 * h = e & h * g9 = e ) ) by GROUP_1:def 2;
consider h being Element of (G . i) such that
A24: ( g * h = e & h * g = e ) by A23;
A25: e = 1_ (G . i) by A23, GROUP_1:def 4;
then A26: [i,h] = (Rev q) . (len p) by A5, A22, A24
.= (Rev q) . (len (Rev q)) by A4, FINSEQ_5:def 3
.= (Rev q) . ((len q9) + 1) by A7, FINSEQ_2:16
.= z2 by A7, FINSEQ_1:42 ;
p ^ q = p9 ^ (<*z1*> ^ (<*z2*> ^ (Rev q9))) by A6, A10, FINSEQ_1:32
.= p9 ^ ((<*z1*> ^ <*z2*>) ^ (Rev q9)) by FINSEQ_1:32
.= (p9 ^ (<*[i,g]*> ^ <*z2*>)) ^ (Rev q9) by A21, FINSEQ_1:32
.= (p9 ^ <*[i,g],[i,h]*>) ^ (Rev q9) by A26, FINSEQ_1:def 9 ;
then ReductionRel G reduces p ^ q,p9 ^ (Rev q9) by A24, A25, Th32;
hence ReductionRel G reduces p ^ q, {} by A20, REWRITE1:16; :: thesis: verum

end;

A27: for n being Nat holds S₂[n] from NAT_1:sch 2(A1, A2);
let p, q be FinSequence of FreeAtoms G; :: thesis: ( 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] ) implies ReductionRel G reduces p ^ q, {} )
assume ( 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] ) ) ; :: thesis: ReductionRel G reduces p ^ q, {}
hence ReductionRel G reduces p ^ q, {} by A27; :: thesis: verum