reconsider f = <*2,3,1*> as Permutation of (Seg 3) by ;
ex l being FinSequence of () 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 () by ;
reconsider l = <*l2,l1*> as FinSequence of () ;
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 = l2 * l1 by GROUP_4:10
.= L1 * L2 by MATRIX_1:def 13
.= <*2,3,1*> 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 ;
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 ;
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 ;
A5: len () = 3 by MATRIX_1:9;
l . i = <*2,1,3*> by ;
then q is being_transposition by ;
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 ;
A7: len () = 3 by MATRIX_1:9;
l . i = <*1,3,2*> by ;
then q is being_transposition by ;
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 <*2,3,1*> is even Permutation of (Seg 3) by MATRIX_1:def 15; :: thesis: verum