let a, b be Integer; :: thesis: Oddity (a * b) = (Oddity a) * (Oddity b)

per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose ( a = 0 or b = 0 ) ; :: thesis: Oddity (a * b) = (Oddity a) * (Oddity b)

hence Oddity (a * b) = (Oddity a) * (Oddity b) ; :: thesis: verum

end;

suppose B1: ( a <> 0 & b <> 0 ) ; :: thesis: Oddity (a * b) = (Oddity a) * (Oddity b)

then reconsider a = a as non zero Integer ;
reconsider b = b as non zero Integer by B1;
((Oddity a) * (Oddity b)) * (Parity (a * b)) = ((Oddity a) * (Oddity b)) * ((Parity a) * (Parity b)) by ILP
.= ((Oddity a) * (Parity a)) * ((Oddity b) * (Parity b))
.= (Oddity (a * b)) * (Parity (a * b)) ;
hence Oddity (a * b) = (Oddity a) * (Oddity b) by XCMPLX_1:5; :: thesis: verum

end;

end;