defpred S₁[ non zero 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:97;
A3: (Bin1 1) /. 1 = k by A2, FINSEQ_4:16;
1 in Seg 1 by FINSEQ_1:3;
then Bin1 1 = <*TRUE*> by A2, A3, Th5;
hence S₁[1] by Th2; :: thesis: verum

end;

A4: now :: thesis: for m being non zero Nat st S₁[m] holds
S₁[m + 1]

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

end;

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