let a be Integer; :: thesis: |.(Oddity a).| = Oddity |.a.|

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

suppose a = 0 ; :: thesis: |.(Oddity a).| = Oddity |.a.|

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

end;

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

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

end;

end;