defpred S₁[ Nat] means Absval (Bin1 $1) = 1;
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: Absval (Bin1 n) = 1 ; :: thesis: S₁[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;

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