let n be Nat; :: thesis: ( n >= 2 implies ex k being positive Nat st (2 |^ n) - 1 = (4 * k) - 1 )
defpred S₁[ Nat] means ( $1 >= 2 implies ex k being positive Nat st (2 |^ $1) - 1 = (4 * k) - 1 );
A1: S₁[2]

proof

assume 2 >= 2 ; :: thesis: ex k being positive Nat st (2 |^ 2) - 1 = (4 * k) - 1
take 1 ; :: thesis: (2 |^ 2) - 1 = (4 * 1) - 1
thus (2 |^ 2) - 1 = (4 * 1) - 1 by Lm2; :: thesis: verum

end;

A2: for j being Nat st 2 <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( 2 <= j & S₁[j] implies S₁[j + 1] )
assume A3: 2 <= j ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume S₁[j] ; :: thesis: S₁[j + 1]
then consider k being positive Nat such that
A4: (2 |^ j) - 1 = (4 * k) - 1 by A3;
assume j + 1 >= 2 ; :: thesis: ex k being positive Nat st (2 |^ (j + 1)) - 1 = (4 * k) - 1
take 2 * k ; :: thesis: (2 |^ (j + 1)) - 1 = (4 * (2 * k)) - 1
2 |^ (j + 1) = (2 |^ j) * 2 by NEWTON:6;
hence (2 |^ (j + 1)) - 1 = (4 * (2 * k)) - 1 by A4; :: thesis: verum

end;

for i being Nat st 2 <= i holds
S₁[i] from NAT_1:sch 8(A1, A2);
hence ( n >= 2 implies ex k being positive Nat st (2 |^ n) - 1 = (4 * k) - 1 ) ; :: thesis: verum