defpred S₁[ Nat] means for f being FinSequence of (Group_of_Perm 3) st len f = 2 * $1 & ( for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ) & not Product f = <*1,2,3*> & not Product f = <*2,3,1*> holds
Product f = <*3,1,2*>;
let l be FinSequence of (Group_of_Perm 3); :: thesis: ( (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) & not Product l = <*1,2,3*> & not Product l = <*2,3,1*> implies Product l = <*3,1,2*> )
assume that
A1: (len l) mod 2 = 0 and
A2: for i being Element of NAT st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; :: thesis: ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> )
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let f be FinSequence of (Group_of_Perm 3); :: thesis: ( len f = 2 * (k + 1) & ( for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ) & not Product f = <*1,2,3*> & not Product f = <*2,3,1*> implies Product f = <*3,1,2*> )
assume that
A5: len f = 2 * (k + 1) and
A6: for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
reconsider k = k as Element of NAT by ORDINAL1:def 12;
set l = 2 * k;
A7: 1 <= (2 * k) + 1 by NAT_1:11;
rng (f | (Seg (2 * k))) c= the carrier of (Group_of_Perm 3) by RELAT_1:def 19;
then reconsider g = f | (Seg (2 * k)) as FinSequence of (Group_of_Perm 3) by FINSEQ_1:def 4;
A8: 2 * k <= (2 * k) + 1 by NAT_1:11;
A9: (f | (Seg ((2 * k) + 1))) | (Seg (2 * k)) = (f | ((2 * k) + 1)) | (2 * k)
.= f | (2 * k) by A8, FINSEQ_5:77
.= f | (Seg (2 * k)) ;
A10: dom g c= dom f by RELAT_1:60;
A11: for i being Element of NAT st i in dom g holds
ex q being Element of Permutations 3 st
( g . i = q & q is being_transposition )

proof

let i be Element of NAT ; :: thesis: ( i in dom g implies ex q being Element of Permutations 3 st
( g . i = q & q is being_transposition ) )
assume A12: i in dom g ; :: thesis: ex q being Element of Permutations 3 st
( g . i = q & q is being_transposition )
then consider q being Element of Permutations 3 such that
A13: ( f . i = q & q is being_transposition ) by A6, A10;
take q ; :: thesis: ( g . i = q & q is being_transposition )
thus ( g . i = q & q is being_transposition ) by A12, A13, FUNCT_1:47; :: thesis: verum

end;

set h = f | (Seg ((2 * k) + 1));
len f = ((2 * k) + 1) + 1 by A5;
then len (f | (Seg ((2 * k) + 1))) = (2 * k) + 1 by FINSEQ_3:53;
then A14: f | (Seg ((2 * k) + 1)) = ((f | (Seg ((2 * k) + 1))) | (Seg (2 * k))) ^ <*((f | (Seg ((2 * k) + 1))) . ((2 * k) + 1))*> by FINSEQ_3:55;
A15: dom f = Seg (2 * (k + 1)) by A5, FINSEQ_1:def 3;
(2 * k) + 1 <= (2 * k) + 2 by XREAL_1:6;
then 1 <= (2 * k) + 2 by A7, XXREAL_0:2;
then A16: (2 * k) + 2 in dom f by A15;
then consider q1 being Element of Permutations 3 such that
A17: f . ((2 * k) + 2) = q1 and
A18: q1 is being_transposition by A6;
A19: f . (((2 * k) + 1) + 1) = f /. ((2 * k) + 2) by A16, PARTFUN1:def 6;
(2 * k) + 1 <= (2 * k) + 2 by XREAL_1:6;
then A20: (2 * k) + 1 in dom f by A15, A7;
then consider q2 being Element of Permutations 3 such that
A21: f . ((2 * k) + 1) = q2 and
A22: q2 is being_transposition by A6;
reconsider q12 = q1 * q2 as Element of Permutations 3 by Th39;
(f | (Seg ((2 * k) + 1))) . ((2 * k) + 1) = f . ((2 * k) + 1) by FINSEQ_1:4, FUNCT_1:49;
then A23: (f | (Seg ((2 * k) + 1))) . ((2 * k) + 1) = f /. ((2 * k) + 1) by A20, PARTFUN1:def 6;
f = (f | (Seg ((2 * k) + 1))) ^ <*(f . (((2 * k) + 1) + 1))*> by A5, FINSEQ_3:55;
then f = g ^ (<*(f /. ((2 * k) + 1))*> ^ <*(f /. ((2 * k) + 2))*>) by A14, A9, A23, A19, FINSEQ_1:32;
then A24: Product f = (Product g) * (Product (<*(f /. ((2 * k) + 1))*> ^ <*(f /. ((2 * k) + 2))*>)) by GROUP_4:5
.= (Product g) * ((Product <*(f /. ((2 * k) + 1))*>) * (f /. ((2 * k) + 2))) by GROUP_4:6
.= (Product g) * ((f /. ((2 * k) + 1)) * (f /. ((2 * k) + 2))) by GROUP_4:9 ;
reconsider Pg = Product g as Element of Permutations 3 by MATRIX_1:def 13;
Product g in the carrier of (Group_of_Perm 3) ;
then Product g in Permutations 3 by MATRIX_1:def 13;
then A25: Product g is Permutation of (Seg 3) by MATRIX_1:def 12;
A26: len (Permutations 3) = 3 by MATRIX_1:9;
then A27: ( q1 = <*2,1,3*> or q1 = <*1,3,2*> or q1 = <*3,2,1*> ) by A18, Th38;
A28: q1 = f /. ((2 * k) + 2) by A16, A17, PARTFUN1:def 6;
q1 * q2 in Permutations 3 by Th39;
then A29: q1 * q2 is Permutation of (Seg 3) by MATRIX_1:def 12;
q2 = f /. ((2 * k) + 1) by A20, A21, PARTFUN1:def 6;
then A30: (f /. ((2 * k) + 1)) * (f /. ((2 * k) + 2)) = q1 * q2 by A28, MATRIX_7:9;
then A31: Product f = q12 * Pg by A24, MATRIX_7:9;
2 * k <= (2 * k) + 2 by NAT_1:11;
then Seg (2 * k) c= Seg (2 * (k + 1)) by FINSEQ_1:5;
then dom g = Seg (2 * k) by A15, RELAT_1:62;
then A32: len g = 2 * k by FINSEQ_1:def 3;
then A33: ( Product g = <*1,2,3*> or Product g = <*2,3,1*> or Product g = <*3,1,2*> ) by A4, A11;
( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )

proof

per cases ( ( Pg = <*1,2,3*> & q1 * q2 = <*2,3,1*> ) or ( Pg = <*2,3,1*> & q1 * q2 = <*2,3,1*> ) or ( Pg = <*2,3,1*> & q1 * q2 = <*3,1,2*> ) or q1 * q2 = <*1,2,3*> or ( Pg = <*1,2,3*> & q1 * q2 = <*3,1,2*> ) or ( Pg = <*3,1,2*> & q1 * q2 = <*2,3,1*> ) or ( Pg = <*3,1,2*> & q1 * q2 = <*3,1,2*> ) ) by A4, A32, A11, A22, A26, A27, Th37, Th38;

suppose ( Pg = <*1,2,3*> & q1 * q2 = <*2,3,1*> ) ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )

hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A29, A31, Lm15; :: thesis: verum

end;

suppose ( Pg = <*2,3,1*> & q1 * q2 = <*2,3,1*> ) ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )

hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A24, A30, Th37, MATRIX_7:9; :: thesis: verum

end;

suppose ( Pg = <*2,3,1*> & q1 * q2 = <*3,1,2*> ) ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )

hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A31, Th37; :: thesis: verum

end;

suppose q1 * q2 = <*1,2,3*> ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )

hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A33, A25, A31, Lm16; :: thesis: verum

end;

suppose ( Pg = <*1,2,3*> & q1 * q2 = <*3,1,2*> ) ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )

hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A29, A31, Lm15; :: thesis: verum

end;

suppose ( Pg = <*3,1,2*> & q1 * q2 = <*2,3,1*> ) ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )

hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A31, Th37; :: thesis: verum

end;

suppose ( Pg = <*3,1,2*> & q1 * q2 = <*3,1,2*> ) ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )

hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A24, A30, Th37, MATRIX_7:9; :: thesis: verum

end;

end;

end;

hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) ; :: thesis: verum

end;

A34: S₁[ 0 ]

proof

set G = Group_of_Perm 3;
let f be FinSequence of (Group_of_Perm 3); :: thesis: ( len f = 2 * 0 & ( for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ) & not Product f = <*1,2,3*> & not Product f = <*2,3,1*> implies Product f = <*3,1,2*> )
assume that
A35: len f = 2 * 0 and
for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ; :: thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
A36: 1_ (Group_of_Perm 3) = <*1,2,3*> by FINSEQ_2:53, MATRIX_1:15;
f = <*> the carrier of (Group_of_Perm 3) by A35;
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A36, GROUP_4:8; :: thesis: verum

end;

A37: for s being Nat holds S₁[s] from NAT_1:sch 2(A34, A3);
ex t being Nat st
( len l = (2 * t) + 0 & 0 < 2 ) by A1, NAT_D:def 2;
hence ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> ) by A2, A37; :: thesis: verum