defpred S1[ Nat] means for f being FinSequence of () 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 (); :: 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
let f be FinSequence of (); :: 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 () by RELAT_1:def 19;
then reconsider g = f | (Seg (2 * k)) as FinSequence of () 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
.= 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 ;
take q ; :: thesis: ( g . i = q & q is being_transposition )
thus ( g . i = q & q is being_transposition ) by ; :: 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 ;
(2 * k) + 1 <= (2 * k) + 2 by XREAL_1:6;
then 1 <= (2 * k) + 2 by ;
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 ;
(2 * k) + 1 <= (2 * k) + 2 by XREAL_1:6;
then A20: (2 * k) + 1 in dom f by ;
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 ;
then A23: (f | (Seg ((2 * k) + 1))) . ((2 * k) + 1) = f /. ((2 * k) + 1) by ;
f = (f | (Seg ((2 * k) + 1))) ^ <*(f . (((2 * k) + 1) + 1))*> by ;
then f = g ^ (<*(f /. ((2 * k) + 1))*> ^ <*(f /. ((2 * k) + 2))*>) by ;
then A24: Product f = () * (Product (<*(f /. ((2 * k) + 1))*> ^ <*(f /. ((2 * k) + 2))*>)) by GROUP_4:5
.= () * ((Product <*(f /. ((2 * k) + 1))*>) * (f /. ((2 * k) + 2))) by GROUP_4:6
.= () * ((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 () ;
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 () = 3 by MATRIX_1:9;
then A27: ( q1 = <*2,1,3*> or q1 = <*1,3,2*> or q1 = <*3,2,1*> ) by ;
A28: q1 = f /. ((2 * k) + 2) by ;
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 ;
then A30: (f /. ((2 * k) + 1)) * (f /. ((2 * k) + 2)) = q1 * q2 by ;
then A31: Product f = q12 * Pg by ;
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 ;
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 ;
( 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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ; :: 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: S1[ 0 ]
proof
set G = Group_of_Perm 3;
let f be FinSequence of (); :: 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_ () = <*1,2,3*> by ;
f = <*> the carrier of () by A35;
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by ; :: thesis: verum
end;
A37: for s being Nat holds S1[s] from NAT_1:sch 2(A34, A3);
ex t being Nat st
( len l = (2 * t) + 0 & 0 < 2 ) by ;
hence ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> ) by ; :: thesis: verum