defpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[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

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

S

proof

A34:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[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 )

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*> )

end;assume A4: S

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

set h = f | (Seg ((2 * k) + 1));
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;( 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

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
end;

hence
( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
; :: thesis: verumper 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;

end;

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;proof

A37:
for s being Nat holds S
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;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

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