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

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

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

then ( ( Parity a = 0 or Parity b = 0 ) & Parity (a * b) = 0 ) by Def1;
hence Parity (a * b) = (Parity a) * (Parity b) ; :: thesis: verum

end;

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

then B2: ( Parity b = 2 |^ (2 |-count b) & Parity a = 2 |^ (2 |-count a) ) by Def1;
Parity (a * b) = 2 |^ (2 |-count (a * b)) by B1, Def1
.= 2 |^ ((2 |-count a) + (2 |-count b)) by B1, NEWTON03:57, INT_2:28
.= (2 |^ (2 |-count a)) * (2 |^ (2 |-count b)) by NEWTON:8 ;
hence Parity (a * b) = (Parity a) * (Parity b) by B2; :: thesis: verum

end;

end;