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;
A4: 1 in Seg 1 by FINSEQ_1:5;
A5: Bin1 1 = <*TRUE *> by A2, A3, A4, Th7;
thus S₁[1] by A5, Th4; :: thesis: verum

end;

A6: now

let m be non empty Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A7: S₁[m] ; :: thesis: S₁[m + 1]
A8: ((Bin1 m) ^ <*FALSE *>) /. (m + 1) = FALSE by BINARITH:3;
A9: Absval ((Bin1 m) ^ <*FALSE *>) = 1 by A7, A8, Def3;
A10: ((Bin1 (m + 1)) ^ <*FALSE *>) /. ((m + 1) + 1) = FALSE by BINARITH:3;
A11: Intval ((Bin1 (m + 1)) ^ <*FALSE *>) = Absval ((Bin1 (m + 1)) ^ <*FALSE *>) by A10, 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 A9, FUNCOP_1:def 8
.= 1 ;
thus S₁[m + 1] by A11; :: thesis: verum

end;

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