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

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

hence
Product l is even Permutation of (Seg n)
by MATRIX_1:def 15; :: thesis: verum
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;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