let a be Integer; :: thesis: ( Parity (a + (Parity a)) = (Parity ((Oddity a) + 1)) * (Parity a) & Parity (a - (Parity a)) = (Parity ((Oddity a) - 1)) * (Parity a) )

per cases ( not a is zero or a is zero ) ;

suppose not a is zero ; :: thesis: ( Parity (a + (Parity a)) = (Parity ((Oddity a) + 1)) * (Parity a) & Parity (a - (Parity a)) = (Parity ((Oddity a) - 1)) * (Parity a) )

then reconsider a = a as non zero Integer ;
A1: Parity (a - (Parity a)) = Parity (((Oddity a) * (Parity a)) - (1 * (Parity a)))
.= Parity (((Oddity a) - 1) * (Parity a))
.= (Parity ((Oddity a) - 1)) * (Parity (Parity a)) by ILP
.= (Parity ((Oddity a) - 1)) * (Parity a) ;
Parity (a + (Parity a)) = Parity (((Oddity a) * (Parity a)) + (Parity a))
.= Parity (((Oddity a) + 1) * (Parity a))
.= (Parity ((Oddity a) + 1)) * (Parity (Parity a)) by ILP
.= (Parity ((Oddity a) + 1)) * (Parity a) ;
hence ( Parity (a + (Parity a)) = (Parity ((Oddity a) + 1)) * (Parity a) & Parity (a - (Parity a)) = (Parity ((Oddity a) - 1)) * (Parity a) ) by A1; :: thesis: verum

end;

suppose a is zero ; :: thesis: ( Parity (a + (Parity a)) = (Parity ((Oddity a) + 1)) * (Parity a) & Parity (a - (Parity a)) = (Parity ((Oddity a) - 1)) * (Parity a) )

then ( Parity (a + (Parity a)) = Parity 0 & Parity a = 0 ) by Def1;
hence ( Parity (a + (Parity a)) = (Parity ((Oddity a) + 1)) * (Parity a) & Parity (a - (Parity a)) = (Parity ((Oddity a) - 1)) * (Parity a) ) ; :: thesis: verum

end;

end;