defpred S₁[ non empty Nat] means Intval ((Bin1 $1) ^ <*FALSE *>) = 1;
A1: S₁[1]

proof

consider k being Element of BOOLEAN such that
A2: Bin1 1 = <*k*> by FINSEQ_2:117;
A3: (Bin1 1) /. 1 = k by A2, FINSEQ_4:25;
1 in Seg 1 by FINSEQ_1:5;
then Bin1 1 = <*TRUE *> by A2, A3, Th7;
hence S₁[1] by Th4; :: thesis: verum

end;

A4: now

let m be non empty Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: S₁[m] ; :: thesis: S₁[m + 1]
((Bin1 m) ^ <*FALSE *>) /. (m + 1) = FALSE by BINARITH:3;
then A6: Absval ((Bin1 m) ^ <*FALSE *>) = 1 by A5, Def3;
((Bin1 (m + 1)) ^ <*FALSE *>) /. ((m + 1) + 1) = FALSE by BINARITH:3;
then Intval ((Bin1 (m + 1)) ^ <*FALSE *>) = Absval ((Bin1 (m + 1)) ^ <*FALSE *>) by Def3
.= Absval (((Bin1 m) ^ <*FALSE *>) ^ <*FALSE *>) by Th9
.= (Absval ((Bin1 m) ^ <*FALSE *>)) + (IFEQ FALSE ,FALSE ,0 ,(2 to_power (m + 1))) by BINARITH:46
.= 1 + 0 by A6, FUNCOP_1:def 8
.= 1 ;
hence S₁[m + 1] ; :: thesis: verum

end;

thus for m being non empty Nat holds S₁[m] from NAT_1:sch 10(A1, A4); :: thesis: verum