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

per cases ( a is even or a is odd ) ;

suppose a is even ; :: thesis: parity (a * b) = (parity a) * (parity b)

then ( parity a = 0 & parity (a * b) = 0 ) ;
hence parity (a * b) = (parity a) * (parity b) ; :: thesis: verum

end;

suppose a is odd ; :: thesis: parity (a * b) = (parity a) * (parity b)

then ( parity a = 1 & ( b is even implies a * b is even ) & ( a * b is even implies b is even ) ) ;
hence parity (a * b) = (parity a) * (parity b) ; :: thesis: verum

end;

end;