let a be Integer; :: thesis: for n being non zero Nat holds parity (a |^ n) = parity a
let n be non zero Nat; :: thesis: parity (a |^ n) = parity a

per cases ( a is even or a is odd ) ;

suppose A1: a is even ; :: thesis: parity (a |^ n) = parity a

then a |^ n is even ;
hence parity (a |^ n) = parity a by A1; :: thesis: verum

end;

suppose A1: a is odd ; :: thesis: parity (a |^ n) = parity a

then a |^ n is odd ;
hence parity (a |^ n) = parity a by A1; :: thesis: verum

end;

end;