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

proof

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 )

proof

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 )

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

suppose A4: i = 2 ; :: thesis: ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )

then reconsider q = l . i as Element of Permutations 3 by Th27;
A5: len (Permutations 3) = 3 by MATRIX_1:9;
l . i = <*1,3,2*> by A4;
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;

suppose A6: i = 1 ; :: thesis: ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )

then reconsider q = l . i as Element of Permutations 3 by Th27;
A7: len (Permutations 3) = 3 by MATRIX_1:9;
l . i = <*2,1,3*> by A6;
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;

end;

end;

hence 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 ) ; :: thesis: verum

end;

hence <*3,1,2*> is even Permutation of (Seg 3) by MATRIX_1:def 15; :: thesis: verum