let n be Nat; :: thesis: for l being FinSequence of (Group_of_Perm n) 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 (Group_of_Perm n); :: 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 (Group_of_Perm n) ;
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 (Group_of_Perm n) 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 (Group_of_Perm n) 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