let a, b be Integer; :: thesis: parity (a * b) = min ((parity a),(parity b))
( min ((parity a),(parity b)) = parity a or min ((parity a),(parity b)) = parity b ) by XXREAL_0:def 9;

per cases then ( min ((parity a),(parity b)) = 0 or min ((parity a),(parity b)) = 1 ) by NAT_2:def 1;

suppose B1: min ((parity a),(parity b)) = 0 ; :: thesis: parity (a * b) = min ((parity a),(parity b))

then ( a is even or b is even ) ;
hence parity (a * b) = min ((parity a),(parity b)) by B1; :: thesis: verum

end;

suppose B1: min ((parity a),(parity b)) = 1 ; :: thesis: parity (a * b) = min ((parity a),(parity b))

then ( a is odd & b is odd ) by XXREAL_0:def 9;
then a * b is odd ;
hence parity (a * b) = min ((parity a),(parity b)) by B1; :: thesis: verum

end;

end;