let k, i be Nat; :: thesis: ( k > 0 & i is even implies i |^ k is even )
assume A1: ( k > 0 & i is even ) ; :: thesis: i |^ k is even
defpred S₁[ Nat] means ( $1 > 0 & i is even implies i |^ $1 is even );
A2: S₁[ 0 ] ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
S₁[n + 1]

proof

now

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

suppose n = 0 ; :: thesis: S₁[n + 1]

hence S₁[n + 1] by NEWTON:10; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: S₁[n + 1]

(i |^ n) * i is even by A1;
hence S₁[n + 1] by NEWTON:11; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence i |^ k is even by A1; :: thesis: verum