:: deftheorem Def1 defines Parity NEWTON05:def 3 :
for a being Integer holds
( ( a = 0 implies Parity a = 0 ) & ( not a = 0 implies Parity a = 2 |^ (2 |-count a) ) );