let n be Nat; :: thesis:
let p, q be Element of Permutations n; :: thesis:
reconsider pq = p * q as Element of Permutations n by MATRIX_9:39;

now :: thesis:

per cases ;

suppose A1: n < 2 ; :: thesis:

then pq is even by Lm3;
hence ( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) iff p * q is even ) by A1, Lm3; :: thesis:

end;

suppose n >= 2 ; :: thesis:

then reconsider n2 = n - 2 as Nat by NAT_1:21;
set K = the non degenerated commutative Fanoian domRing-like Ring;
reconsider p9 = p, q9 = q, pq = pq as Element of Permutations (n2 + 2) ;
thus ( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) implies p * q is even ) :: thesis:

proof

assume ( ( p is even & q is even ) or ( p is odd & q is odd ) ) ; :: thesis:
then ( ( sgn (p9, the non degenerated commutative Fanoian domRing-like Ring) = 1_ the non degenerated commutative Fanoian domRing-like Ring & sgn (q9, the non degenerated commutative Fanoian domRing-like Ring) = 1_ the non degenerated commutative Fanoian domRing-like Ring ) or ( sgn (p9, the non degenerated commutative Fanoian domRing-like Ring) = - (1_ the non degenerated commutative Fanoian domRing-like Ring) & sgn (q9, the non degenerated commutative Fanoian domRing-like Ring) = - (1_ the non degenerated commutative Fanoian domRing-like Ring) ) ) by Th23;
then A2: (sgn (p9, the non degenerated commutative Fanoian domRing-like Ring)) * (sgn (q9, the non degenerated commutative Fanoian domRing-like Ring)) = (1_ the non degenerated commutative Fanoian domRing-like Ring) * (1_ the non degenerated commutative Fanoian domRing-like Ring) by VECTSP_1:10;
sgn (pq, the non degenerated commutative Fanoian domRing-like Ring) = 1_ the non degenerated commutative Fanoian domRing-like Ring by A2, Th24;
hence p * q is even by Th23; :: thesis:

end;

thus ( not p * q is even or ( p is even & q is even ) or ( p is odd & q is odd ) ) :: thesis:

proof

assume p * q is even ; :: thesis:
then sgn (pq, the non degenerated commutative Fanoian domRing-like Ring) = 1_ the non degenerated commutative Fanoian domRing-like Ring by Th23;
then A3: (sgn (p9, the non degenerated commutative Fanoian domRing-like Ring)) * (sgn (q9, the non degenerated commutative Fanoian domRing-like Ring)) = 1_ the non degenerated commutative Fanoian domRing-like Ring by Th24;
assume A4: ( not ( p is even & q is even ) & not ( p is odd & q is odd ) ) ; :: thesis:

now :: thesis:

per cases by A4;

suppose A5: ( p is even & q is odd ) ; :: thesis:

then A6: sgn (q9, the non degenerated commutative Fanoian domRing-like Ring) = - (1_ the non degenerated commutative Fanoian domRing-like Ring) by Th23;
sgn (p9, the non degenerated commutative Fanoian domRing-like Ring) = 1_ the non degenerated commutative Fanoian domRing-like Ring by A5, Th23;
then (sgn (p9, the non degenerated commutative Fanoian domRing-like Ring)) * (sgn (q9, the non degenerated commutative Fanoian domRing-like Ring)) = - (1_ the non degenerated commutative Fanoian domRing-like Ring) by A6;
hence contradiction by A3, Th22; :: thesis:

end;

suppose A7: ( p is odd & q is even ) ; :: thesis:

then A8: sgn (q9, the non degenerated commutative Fanoian domRing-like Ring) = 1_ the non degenerated commutative Fanoian domRing-like Ring by Th23;
sgn (p9, the non degenerated commutative Fanoian domRing-like Ring) = - (1_ the non degenerated commutative Fanoian domRing-like Ring) by A7, Th23;
then (sgn (p9, the non degenerated commutative Fanoian domRing-like Ring)) * (sgn (q9, the non degenerated commutative Fanoian domRing-like Ring)) = - (1_ the non degenerated commutative Fanoian domRing-like Ring) by A8;
hence contradiction by A3, Th22; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

end;

hence ( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) iff p * q is even ) ; :: thesis: