theorem :: MATRIX_9:40

for n being Nat
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)