per cases ( a is zero or a <> 0 ) ;

suppose a is zero ; :: thesis: Oddity (Oddity a) = Oddity a

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

end;

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

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

end;

end;