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;
consider K being 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,K = 1_ K & sgn q9,K = 1_ K ) or ( sgn p9,K = - (1_ K) & sgn q9,K = - (1_ K) ) ) by Th23;
then A2: (sgn p9,K) * (sgn q9,K) = (1_ K) * (1_ K) by VECTSP_1:42;
(1_ K) * (1_ K) = 1_ K by VECTSP_1:def 13;
then sgn pq,K = 1_ K 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,K = 1_ K by Th23;
then A3: (sgn p9,K) * (sgn q9,K) = 1_ K 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,K = - (1_ K) by Th23;
sgn p9,K = 1_ K by A5, Th23;
then (sgn p9,K) * (sgn q9,K) = - (1_ K) by A6, VECTSP_1:def 13;
hence contradiction by A3, Th22; :: thesis: verum

end;

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

then A8: sgn q9,K = 1_ K by Th23;
sgn p9,K = - (1_ K) by A7, Th23;
then (sgn p9,K) * (sgn q9,K) = - (1_ K) by A8, VECTSP_1:def 13;
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