defpred S₁[ Nat] means ($1 + 1) ^2 < 2 to_power $1;
A1: for k being Nat st k >= 6 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 6 & S₁[k] implies S₁[k + 1] )
assume that
A2: k >= 6 and
A3: (k + 1) ^2 < 2 to_power k ; :: thesis: S₁[k + 1]
k >= 4 by A2, XXREAL_0:2;
then (2 * k) + 3 < 2 to_power k by Lm7;
then A4: ((k + 1) ^2) + ((2 * k) + 3) < ((k + 1) ^2) + (2 to_power k) by XREAL_1:6;
((k + 1) ^2) + (2 to_power k) < (2 to_power k) + (2 to_power k) by A3, XREAL_1:6;
then ((k + 1) + 1) ^2 < 2 * (2 to_power k) by A4, XXREAL_0:2;
then ((k + 1) + 1) ^2 < (2 to_power 1) * (2 to_power k) by POWER:25;
hence S₁[k + 1] by POWER:27; :: thesis: verum

end;

A5: S₁[6] by POWER:64;
for n being Nat st n >= 6 holds
S₁[n] from NAT_1:sch 8(A5, A1);
hence for n being Element of NAT st n >= 6 holds
(n + 1) ^2 < 2 to_power n ; :: thesis: verum