defpred S₁[ non zero Nat] means for F being Tuple of $1, BOOLEAN holds Absval F < 2 to_power $1;
A1: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
n < n + 1 by NAT_1:13;
then A3: 2 to_power n < 2 to_power (n + 1) by POWER:39;
let F be Tuple of n + 1, BOOLEAN ; :: thesis: Absval F < 2 to_power (n + 1)
consider T being Element of n -tuples_on BOOLEAN, d being Element of BOOLEAN such that
A4: F = T ^ <*d*> by FINSEQ_2:117;
A5: Absval F = (Absval T) + (IFEQ (d,FALSE,0,(2 to_power n))) by A4, BINARITH:20;
A6: Absval T < 2 to_power n by A2;

per cases ( d = FALSE or d = TRUE ) by XBOOLEAN:def 3;

suppose d = FALSE ; :: thesis: Absval F < 2 to_power (n + 1)

then Absval F = (Absval T) + 0 by A5, FUNCOP_1:def 8;
then (Absval F) + (2 to_power n) < (2 to_power n) + (2 to_power (n + 1)) by A2, A3, XREAL_1:8;
hence Absval F < 2 to_power (n + 1) by XREAL_1:6; :: thesis: verum

end;

suppose d = TRUE ; :: thesis: Absval F < 2 to_power (n + 1)

then Absval F = (Absval T) + (2 to_power n) by A5, FUNCOP_1:def 8;
then Absval F < (2 to_power n) + (2 to_power n) by A6, XREAL_1:6;
then Absval F < (2 to_power n) * 2 ;
then Absval F < (2 to_power n) * (2 to_power 1) by POWER:25;
hence Absval F < 2 to_power (n + 1) by POWER:27; :: thesis: verum

end;

end;

end;

A7: S₁[1]

proof

let F be Tuple of 1, BOOLEAN ; :: thesis: Absval F < 2 to_power 1
consider d being Element of BOOLEAN such that
A8: F = <*d*> by FINSEQ_2:97;
( d = TRUE or d = FALSE ) by XBOOLEAN:def 3;
then ( Absval F = 1 or Absval F = 0 ) by A8, BINARITH:15, BINARITH:16;
then Absval F < 2 ;
hence Absval F < 2 to_power 1 by POWER:25; :: thesis: verum

end;

thus for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A7, A1); :: thesis: verum