A1: a is Nat by TARSKI:1;
defpred S₁[ Nat] means k |^ k is Integer;
A2: for a being Nat st S₁[a] holds
S₁[a + 1]

proof

let a be Nat; :: thesis: ( S₁[a] implies S₁[a + 1] )
assume k |^ a is Integer ; :: thesis: S₁[a + 1]
then reconsider b = k |^ a as Integer ;
k |^ (a + 1) = k * b by NEWTON:6;
hence S₁[a + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ] by NEWTON:4;
for a being Nat holds S₁[a] from NAT_1:sch 2(A3, A2);
hence k |^ a is integer by A1; :: thesis: verum