for n being Nat
for p, q being Element of Permutations n holds
( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) iff p * q is even )