let a be Integer; :: thesis: for n being Nat holds Parity (a |^ n) = (Parity a) |^ n
let n be Nat; :: thesis: Parity (a |^ n) = (Parity a) |^ n
defpred S₁[ Nat] means Parity (a |^ $1) = (Parity a) |^ $1;
A1: S₁[ 0 ]

proof

Parity (1 * (a |^ 0)) = 1 * ((Parity a) |^ 0) ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: Parity (a |^ k) = (Parity a) |^ k ; :: thesis: S₁[k + 1]
Parity (a |^ (k + 1)) = Parity (a * (a |^ k)) by NEWTON:6
.= (Parity a) * ((Parity a) |^ k) by B1, ILP ;
hence S₁[k + 1] by NEWTON:6; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A1, A2);
hence Parity (a |^ n) = (Parity a) |^ n ; :: thesis: verum