let n be Nat; :: thesis: 2 |^ (n + 1) = (2 |^ n) + (2 |^ n)
defpred S₁[ Nat] means 2 |^ ($1 + 1) = (2 |^ $1) + (2 |^ $1);
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: 2 |^ (m + 1) = (2 |^ m) + (2 |^ m) ; :: thesis: S₁[m + 1]
(2 |^ (m + 1)) + (2 |^ (m + 1)) = (2 * (2 |^ m)) + (2 |^ (m + 1)) by NEWTON:6
.= (2 * (2 |^ m)) + (2 * (2 |^ m)) by NEWTON:6
.= 2 * ((2 |^ m) + (2 |^ m))
.= 2 |^ ((m + 1) + 1) by A2, NEWTON:6 ;
hence S₁[m + 1] ; :: thesis: verum

end;

2 |^ (0 + 1) = 1 + 1
.= (2 |^ 0) + 1 by NEWTON:4
.= (2 |^ 0) + (2 |^ 0) by NEWTON:4 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence 2 |^ (n + 1) = (2 |^ n) + (2 |^ n) ; :: thesis: verum