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

suppose a = 0 ; :: thesis: (Parity a) * (Oddity a) = a

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

end;

suppose a <> 0 ; :: thesis: (Parity a) * (Oddity a) = a

hence (Parity a) * (Oddity a) = a by XCMPLX_1:87; :: thesis: verum

end;

end;