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

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

hence Parity (Parity a) = Parity a by Def1; :: thesis: verum

end;

suppose not a is zero ; :: thesis: Parity (Parity a) = Parity a

then reconsider a = a as non zero Integer ;
2 |^ (2 |-count a) = Parity (2 |^ (2 |-count a))
.= Parity (Parity a) by Def1 ;
hence Parity (Parity a) = Parity a by Def1; :: thesis: verum

end;

end;