let i, k be Nat; :: thesis: ( k > 0 & i is even implies i |^ k is even )
assume that
A1: k > 0 and
A2: i is even ; :: thesis: i |^ k is even
defpred S₁[ Nat] means ( $1 > 0 & i is even implies i |^ $1 is even );
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 :: thesis: S₁[n + 1]

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

end;

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

end;

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

end;

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