defpred S₁[ Nat] means for F being Tuple of $1, BOOLEAN st F = 0* $1 holds
Absval F = 0 ;
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: 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 Th4;
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:60
.= (Absval F1) + (IFEQ (FALSE,FALSE,0,(2 to_power n))) by BINARITH:20
.= 0 + (IFEQ (FALSE,FALSE,0,(2 to_power n))) by A2
.= 0 by FUNCOP_1:def 8 ;
:: thesis: verum

end;

A3: S₁[1] by BINARITH:15, FINSEQ_2:59;
thus for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A3, A1); :: thesis: verum