defpred S₁[ Nat] means for k being Nat st 1 <= k & k <= $1 holds
ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1);
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: S₁[i] ; :: thesis: S₁[i + 1]
let k be Nat; :: thesis: ( 1 <= k & k <= i + 1 implies ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) )
assume that
A3: 1 <= k and
A4: k <= i + 1 ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

now :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

per cases ( ( k = i + 1 & i = 0 ) or ( k = i + 1 & i > 0 ) or k < i + 1 ) by A4, XXREAL_0:1;

suppose A5: ( k = i + 1 & i = 0 ) ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

set m = 0 ;
A6: 1 = 2 |^ 0 by NEWTON:4;
k = 1 * ((0 * 2) + 1) by A5;
hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) by A6; :: thesis: verum

end;

suppose A7: ( k = i + 1 & i > 0 ) ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

per cases ( k mod 2 = 1 or k mod 2 = 0 ) by NAT_D:12;

suppose k mod 2 = 1 ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

then consider m being Nat such that
A8: k = (2 * m) + 1 and
1 < 2 by NAT_D:def 2;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
1 = 2 |^ 0 by NEWTON:4;
then k = (2 |^ 0) * ((2 * m) + 1) by A8;
hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) ; :: thesis: verum

end;

suppose k mod 2 = 0 ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

then consider j being Nat such that
A9: k = (2 * j) + 0 and
0 < 2 by NAT_D:def 2;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
A10: j <= i

proof

assume j > i ; :: thesis: contradiction
then j + j > i + 1 by NAT_1:14, XREAL_1:8;
hence contradiction by A7, A9; :: thesis: verum

end;

j <> 0 by A7, A9;
then j >= 1 by NAT_1:14;
then consider n, m being Nat such that
A11: j = (2 |^ n) * ((2 * m) + 1) by A2, A10;
k = (2 * (2 |^ n)) * ((2 * m) + 1) by A9, A11;
then k = (2 |^ (n + 1)) * ((2 * m) + 1) by NEWTON:6;
hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) ; :: thesis: verum

end;

end;

end;

suppose k < i + 1 ; :: thesis: ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1)

then k <= i by NAT_1:13;
hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) by A2, A3; :: thesis: verum

end;

end;

end;

hence ex n, m being Nat st k = (2 |^ n) * ((2 * m) + 1) ; :: thesis: verum

end;

let i be Nat; :: thesis: ( i > 0 implies ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1) )
assume i > 0 ; :: thesis: ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1)
then A12: i >= 1 by NAT_1:14;
A13: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A1);
hence ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1) by A12; :: thesis: verum