reconsider f = <*3,1,2*> as Permutation of (Seg 3) by Th27, MATRIX_1:def 12;

ex l being FinSequence of (Group_of_Perm 3) st

( (len l) mod 2 = 0 & f = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ) )

ex l being FinSequence of (Group_of_Perm 3) st

( (len l) mod 2 = 0 & f = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ) )

proof

hence
<*3,1,2*> is even Permutation of (Seg 3)
by MATRIX_1:def 15; :: thesis: verum
reconsider l1 = <*2,1,3*>, l2 = <*1,3,2*> as Element of (Group_of_Perm 3) by Th27, MATRIX_1:def 13;

reconsider l = <*l1,l2*> as FinSequence of (Group_of_Perm 3) ;

take l ; :: thesis: ( (len l) mod 2 = 0 & f = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ) )

A1: len l = 2 * 1 by FINSEQ_1:44;

hence (len l) mod 2 = 0 by NAT_D:13; :: thesis: ( f = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ) )

reconsider L2 = l2, L1 = l1 as Element of Permutations 3 by Th27;

Product l = l1 * l2 by GROUP_4:10

.= L2 * L1 by MATRIX_1:def 13

.= <*3,1,2*> by Th37 ;

hence f = Product l ; :: thesis: for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition )

A2: dom l = {1,2} by A1, FINSEQ_1:2, FINSEQ_1:def 3;

for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition )

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ; :: thesis: verum

end;reconsider l = <*l1,l2*> as FinSequence of (Group_of_Perm 3) ;

take l ; :: thesis: ( (len l) mod 2 = 0 & f = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ) )

A1: len l = 2 * 1 by FINSEQ_1:44;

hence (len l) mod 2 = 0 by NAT_D:13; :: thesis: ( f = Product l & ( for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ) )

reconsider L2 = l2, L1 = l1 as Element of Permutations 3 by Th27;

Product l = l1 * l2 by GROUP_4:10

.= L2 * L1 by MATRIX_1:def 13

.= <*3,1,2*> by Th37 ;

hence f = Product l ; :: thesis: for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition )

A2: dom l = {1,2} by A1, FINSEQ_1:2, FINSEQ_1:def 3;

for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition )

proof

hence
for i being Nat st i in dom l holds
let i be Nat; :: thesis: ( i in dom l implies ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) )

assume A3: i in dom l ; :: thesis: ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition )

end;( l . i = q & q is being_transposition ) )

assume A3: i in dom l ; :: thesis: ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition )

per cases
( i = 2 or i = 1 )
by A2, A3, TARSKI:def 2;

end;

suppose A4:
i = 2
; :: thesis: ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition )

( l . i = q & q is being_transposition )

then reconsider q = l . i as Element of Permutations 3 by Th27, FINSEQ_1:44;

A5: len (Permutations 3) = 3 by MATRIX_1:9;

l . i = <*1,3,2*> by A4, FINSEQ_1:44;

then q is being_transposition by A5, Th30;

hence ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ; :: thesis: verum

end;A5: len (Permutations 3) = 3 by MATRIX_1:9;

l . i = <*1,3,2*> by A4, FINSEQ_1:44;

then q is being_transposition by A5, Th30;

hence ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ; :: thesis: verum

suppose A6:
i = 1
; :: thesis: ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition )

( l . i = q & q is being_transposition )

then reconsider q = l . i as Element of Permutations 3 by Th27, FINSEQ_1:44;

A7: len (Permutations 3) = 3 by MATRIX_1:9;

l . i = <*2,1,3*> by A6, FINSEQ_1:44;

then q is being_transposition by A7, Th31;

hence ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ; :: thesis: verum

end;A7: len (Permutations 3) = 3 by MATRIX_1:9;

l . i = <*2,1,3*> by A6, FINSEQ_1:44;

then q is being_transposition by A7, Th31;

hence ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ; :: thesis: verum

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ; :: thesis: verum