defpred S_{1}[ 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_{1}[n] holds

S_{1}[n + 1]
_{1}[1]
by BINARITH:15, FINSEQ_2:59;

thus for n being non zero Nat holds S_{1}[n]
from NAT_1:sch 10(A3, A1); :: thesis: verum

Absval F = 0 ;

A1: for n being non zero Nat st S

S

proof

A3:
S
let n be non zero Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: for F being Tuple of n, BOOLEAN st F = 0* n holds

Absval F = 0 ; :: thesis: S_{1}[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;assume A2: for F being Tuple of n, BOOLEAN st F = 0* n holds

Absval F = 0 ; :: thesis: S

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

thus for n being non zero Nat holds S