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

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
set i1 = i + 1;
A4: ( (1 + n) |^ (i + 1) = ((1 + n) |^ i) * (1 + n) & (n |^ i) * n = n |^ (i + 1) ) by NEWTON:6;
assume S₁[i] ; :: thesis: S₁[i + 1]
then A5: (i + (n |^ i)) * (1 + n) <= (1 + n) |^ (i + 1) by A4, XREAL_1:66;
(i * n) + (n |^ i) >= 0 + 1 by A1, NAT_1:14;
then ((i * n) + (n |^ i)) + (i + (n |^ (i + 1))) >= 1 + (i + (n |^ (i + 1))) by XREAL_1:7;
hence S₁[i + 1] by A4, A5, XXREAL_0:2; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence k + (n |^ k) <= (1 + n) |^ k ; :: thesis: verum