let a be Integer; :: thesis: Parity a = Parity (- a)

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

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

then reconsider a = a as non zero Integer ;
B1: 2 is non trivial Nat by NAT_2:def 1;
Parity (- a) = 2 |^ (2 |-count (a * (- 1))) by Def1
.= 2 |^ ((2 |-count a) + (2 |-count (- 1))) by NEWTON03:57, INT_2:28
.= 2 |^ ((2 |-count a) + 0) by B1 ;
hence Parity a = Parity (- a) by Def1; :: thesis: verum

end;

suppose a = 0 ; :: thesis: Parity a = Parity (- a)

hence Parity a = Parity (- a) ; :: thesis: verum

end;

end;