let n be Nat; :: thesis: for p, q being Element of Permutations n holds
( ( ( p is even & q is even ) or ( not p is even & not q is even ) ) iff p * q is even )
let p, q be Element of Permutations n; :: thesis: ( ( ( p is even & q is even ) or ( not p is even & not q is even ) ) iff p * q is even )
reconsider pq = p * q as Element of Permutations n by MATRIX_9:39;

now

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

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

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

end;

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

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

proof

assume ( ( p is even & q is even ) or ( not p is even & not q is even ) ) ; :: thesis: p * q is even
then ( ( sgn (p9, the Fanoian Field) = 1_ the Fanoian Field & sgn (q9, the Fanoian Field) = 1_ the Fanoian Field ) or ( sgn (p9, the Fanoian Field) = - (1_ the Fanoian Field) & sgn (q9, the Fanoian Field) = - (1_ the Fanoian Field) ) ) by Th23;
then A2: (sgn (p9, the Fanoian Field)) * (sgn (q9, the Fanoian Field)) = (1_ the Fanoian Field) * (1_ the Fanoian Field) by VECTSP_1:10;
(1_ the Fanoian Field) * (1_ the Fanoian Field) = 1_ the Fanoian Field by VECTSP_1:def 4;
then sgn (pq, the Fanoian Field) = 1_ the Fanoian Field 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 ( not p is even & not q is even ) ) :: thesis: verum

proof

assume p * q is even ; :: thesis: ( ( p is even & q is even ) or ( not p is even & not q is even ) )
then sgn (pq, the Fanoian Field) = 1_ the Fanoian Field by Th23;
then A3: (sgn (p9, the Fanoian Field)) * (sgn (q9, the Fanoian Field)) = 1_ the Fanoian Field by Th24;
assume A4: ( not ( p is even & q is even ) & not ( not p is even & not q is even ) ) ; :: thesis: contradiction

now

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

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

then A6: sgn (q9, the Fanoian Field) = - (1_ the Fanoian Field) by Th23;
sgn (p9, the Fanoian Field) = 1_ the Fanoian Field by A5, Th23;
then (sgn (p9, the Fanoian Field)) * (sgn (q9, the Fanoian Field)) = - (1_ the Fanoian Field) by A6, VECTSP_1:def 4;
hence contradiction by A3, Th22; :: thesis: verum

end;

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

then A8: sgn (q9, the Fanoian Field) = 1_ the Fanoian Field by Th23;
sgn (p9, the Fanoian Field) = - (1_ the Fanoian Field) by A7, Th23;
then (sgn (p9, the Fanoian Field)) * (sgn (q9, the Fanoian Field)) = - (1_ the Fanoian Field) by A8, VECTSP_1:def 4;
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 ( not p is even & not q is even ) ) iff p * q is even ) ; :: thesis: verum