defpred S₁[ Nat] means for z being Tuple of $1,BOOLEAN st z /. $1 = TRUE holds
Absval z >= 2 to_power ($1 -' 1);
A1: S₁[1]

proof

let z be Tuple of 1,BOOLEAN ; :: thesis: ( z /. 1 = TRUE implies Absval z >= 2 to_power (1 -' 1) )
assume A2: z /. 1 = TRUE ; :: thesis: Absval z >= 2 to_power (1 -' 1)
A3: len z = 1 by FINSEQ_1:def 18;
then z . 1 = z /. 1 by FINSEQ_4:24;
then z = <*TRUE *> by A2, A3, FINSEQ_1:57;
then A4: Absval z = 1 by BINARITH:42;
2 to_power (1 -' 1) = 2 to_power (1 - 1) by XREAL_0:def 2;
hence Absval z >= 2 to_power (1 -' 1) by A4, POWER:29; :: thesis: verum

end;

A5: 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 S₁[n] ; :: thesis: S₁[n + 1]
let z be Tuple of (n + 1),BOOLEAN ; :: thesis: ( z /. (n + 1) = TRUE implies Absval z >= 2 to_power ((n + 1) -' 1) )
assume A6: z /. (n + 1) = TRUE ; :: thesis: Absval z >= 2 to_power ((n + 1) -' 1)
consider x being Tuple of n,BOOLEAN , a being Element of BOOLEAN such that
A7: z = x ^ <*a*> by FINSEQ_2:137;
A8: n + 1 >= 1 by NAT_1:11;
then (n + 1) - 1 >= 1 - 1 by XREAL_1:11;
then A9: (n + 1) -' 1 = n by XREAL_0:def 2;
len z = n + 1 by FINSEQ_1:def 18;
then A10: z /. (n + 1) = (x ^ <*a*>) . (n + 1) by A7, A8, FINSEQ_4:24
.= a by FINSEQ_2:136 ;
Absval z = (Absval x) + (IFEQ a,FALSE ,0 ,(2 to_power n)) by A7, BINARITH:46
.= (Absval x) + (2 to_power n) by A6, A10, FUNCOP_1:def 8 ;
hence Absval z >= 2 to_power ((n + 1) -' 1) by A9, NAT_1:11; :: thesis: verum

end;

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