defpred S_{1}[ Nat] means Absval (Bin1 $1) = 1;

A1: for n being non zero Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[1]
by Th10, BINARITH:16;

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

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: Absval (Bin1 n) = 1 ; :: thesis: S_{1}[n + 1]

thus Absval (Bin1 (n + 1)) = Absval ((Bin1 n) ^ <*FALSE*>) by BINARI_2:7

.= (Absval (Bin1 n)) + (IFEQ (FALSE,FALSE,0,(2 to_power n))) by BINARITH:20

.= (Absval (Bin1 n)) + 0 by FUNCOP_1:def 8

.= 1 by A2 ; :: thesis: verum

end;assume A2: Absval (Bin1 n) = 1 ; :: thesis: S

thus Absval (Bin1 (n + 1)) = Absval ((Bin1 n) ^ <*FALSE*>) by BINARI_2:7

.= (Absval (Bin1 n)) + (IFEQ (FALSE,FALSE,0,(2 to_power n))) by BINARITH:20

.= (Absval (Bin1 n)) + 0 by FUNCOP_1:def 8

.= 1 by A2 ; :: thesis: verum

thus for n being non zero Nat holds S