defpred S₁[ Nat] means for F being Tuple of $1, BOOLEAN st F = 0* $1 holds
Absval F = 0 ;
A1: 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 A2: for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval F = 0 ; :: thesis: S₁[n + 1]
let F be Tuple of n + 1, BOOLEAN ; :: thesis: ( F = 0* (n + 1) implies Absval F = 0 )
0* n in BOOLEAN * by Th5;
then 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
then reconsider F1 = 0* n as Tuple of n, BOOLEAN ;
assume F = 0* (n + 1) ; :: thesis: Absval F = 0
hence Absval F = Absval (F1 ^ <*FALSE *>) by FINSEQ_2:74
.= (Absval F1) + (IFEQ FALSE ,FALSE ,0 ,(2 to_power n)) by BINARITH:46
.= 0 + (IFEQ FALSE ,FALSE ,0 ,(2 to_power n)) by A2
.= 0 by FUNCOP_1:def 8 ;
:: thesis: verum

end;

A4: S₁[1] by BINARITH:41, FINSEQ_2:73;
thus for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A4, A1); :: thesis: verum