defpred S₁[ non empty Nat] means for F being Tuple of $1,BOOLEAN holds Absval F < 2 to_power $1;
A1: 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
A2: F = <*d*> by FINSEQ_2:117;
( d = TRUE or d = FALSE ) by XBOOLEAN:def 3;
then ( Absval F = 1 or Absval F = 0 ) by A2, BINARITH:41, BINARITH:42;
then Absval F < 2 ;
hence Absval F < 2 to_power 1 by POWER:30; :: thesis: verum

end;

A3: for n being non empty Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non empty Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let F be Tuple of (n + 1),BOOLEAN ; :: thesis: Absval F < 2 to_power (n + 1)
consider T being Tuple of n,BOOLEAN , d being Element of BOOLEAN such that
A5: F = T ^ <*d*> by FINSEQ_2:137;
A6: Absval F = (Absval T) + (IFEQ d,FALSE ,0 ,(2 to_power n)) by A5, BINARITH:46;
n < n + 1 by NAT_1:13;
then A7: 2 to_power n < 2 to_power (n + 1) by POWER:44;
A8: Absval T < 2 to_power n by A4;

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 A6, FUNCOP_1:def 8;
then (Absval F) + (2 to_power n) < (2 to_power n) + (2 to_power (n + 1)) by A4, A7, XREAL_1:10;
hence Absval F < 2 to_power (n + 1) by XREAL_1:8; :: thesis: verum

end;

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

then Absval F = (Absval T) + (2 to_power n) by A6, FUNCOP_1:def 8;
then Absval F < (2 to_power n) + (2 to_power n) by A8, XREAL_1:8;
then Absval F < (2 to_power n) * 2 ;
then Absval F < (2 to_power n) * (2 to_power 1) by POWER:30;
hence Absval F < 2 to_power (n + 1) by POWER:32; :: thesis: verum

end;

end;

end;

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