:: deftheorem defines even MATRIX_1:def 15 :
for n being Nat
for IT being Permutation of (Seg n) holds
( IT is even iff ex l being FinSequence of (Group_of_Perm n) st
( (len l) mod 2 = 0 & IT = 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 ) ) ) );