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 n < 2 ; :: thesis: ( ( ( p is even & q is even ) or ( not p is even & not q is even ) ) iff p * q is even )

then ( p is even & q is even & 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 ) ; :: 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 p' = p, q' = 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 p',K = 1_ K & sgn q',K = 1_ K ) or ( sgn p',K = - (1_ K) & sgn q',K = - (1_ K) ) ) by Th23;
then ( (sgn p',K) * (sgn q',K) = (1_ K) * (1_ K) & (1_ K) * (1_ K) = 1_ K ) by VECTSP_1:42, VECTSP_1:def 13;
then sgn pq,K = 1_ K by 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 A1: (sgn p',K) * (sgn q',K) = 1_ K by Th24;
assume A2: ( 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 A2;

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

then ( sgn p',K = 1_ K & sgn q',K = - (1_ K) ) by Th23;
then (sgn p',K) * (sgn q',K) = - (1_ K) by VECTSP_1:def 13;
hence contradiction by A1, Th22; :: thesis: verum

end;

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

then ( sgn p',K = - (1_ K) & sgn q',K = 1_ K ) by Th23;
then (sgn p',K) * (sgn q',K) = - (1_ K) by VECTSP_1:def 13;
hence contradiction by A1, 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