defpred S₁[ Nat] means ( 0 <= (2 to_power ($1 -' 1)) - 1 & - (2 to_power ($1 -' 1)) <= 0 );
A1: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A2: 0 <= (2 to_power (k -' 1)) - 1 and
- (2 to_power (k -' 1)) <= 0 ; :: thesis: S₁[k + 1]
(k + 1) -' 1 = k by NAT_D:34;
then 2 to_power (k -' 1) < 2 to_power ((k + 1) -' 1) by NAT_2:9, POWER:39;
hence S₁[k + 1] by A2, XREAL_1:9; :: thesis: verum

end;

1 - 1 = 0 ;
then 2 to_power (1 -' 1) = 2 to_power 0 by XREAL_0:def 2
.= 1 by POWER:24 ;
then A3: S₁[1] ;
thus for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A3, A1); :: thesis: verum