defpred S₁[ Nat] means Absval (Bin1 $1) = 1;
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: Absval (Bin1 n) = 1 ; :: thesis: S₁[n + 1]
thus Absval (Bin1 (n + 1)) = Absval ((Bin1 n) ^ <*FALSE *>) by BINARI_2:9
.= (Absval (Bin1 n)) + (IFEQ FALSE ,FALSE ,0 ,(2 to_power n)) by BINARITH:46
.= (Absval (Bin1 n)) + 0 by FUNCOP_1:def 8
.= 1 by A2 ; :: thesis: verum

end;

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