let n be Nat; :: thesis: 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 )
let p, q be Element of Permutations n; :: thesis: ( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) iff p * q is even )
reconsider pq = p * q as Element of Permutations n by MATRIX_9:39;

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

per cases ( n < 2 or n >= 2 ) ;

suppose A1: n < 2 ; :: thesis: ( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) iff p * q is even )

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: verum

end;

suppose n >= 2 ; :: thesis: ( ( ( ( p is even & q is even ) or ( p is odd & q is odd ) ) implies p * q is even ) & ( not p * q is even or ( p is even & q is even ) or ( p is odd & q is odd ) ) )

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: ( not p * q is even or ( p is even & q is even ) or ( p is odd & q is odd ) )

proof

assume ( ( p is even & q is even ) or ( p is odd & q is odd ) ) ; :: thesis: p * q is even
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: verum

end;

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

proof

assume p * q is even ; :: thesis: ( ( p is even & q is even ) or ( p is odd & q is odd ) )
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: contradiction

now :: thesis: contradiction

per cases ( ( p is even & q is odd ) or ( p is odd & q is even ) ) by A4;

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

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: verum

end;

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

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: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

end;

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