let n be Nat; :: thesis: for l being FinSequence of () st (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) holds
Product l is even Permutation of (Seg n)

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 n st
( l . i = q & q is being_transposition ) ) implies Product l is even Permutation of (Seg n) )

Product l in the carrier of () ;
then Product l in Permutations n by MATRIX_1:def 13;
then reconsider Pf = Product l as Permutation of (Seg n) by MATRIX_1:def 12;
assume A1: ( (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) ) ; :: thesis: Product l is even Permutation of (Seg n)
ex l being FinSequence of the carrier of () st
( (len l) mod 2 = 0 & Pf = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) )
proof
consider l being FinSequence of the carrier of () such that
A2: ( (len l) mod 2 = 0 & Pf = Product l ) and
A3: for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) by A1;
take l ; :: thesis: ( (len l) mod 2 = 0 & Pf = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) )

thus ( (len l) mod 2 = 0 & Pf = Product l ) by A2; :: thesis: for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition )

let i be Nat; :: thesis: ( i in dom l implies ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) )

thus ( i in dom l implies ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) by A3; :: thesis: verum
end;
hence Product l is even Permutation of (Seg n) by MATRIX_1:def 15; :: thesis: verum