let r be Element of INT.Ring; :: thesis: for n being Element of NAT
for i being Integer st i = n holds
i * r = n * r
defpred S₁[ Nat] means for i being Integer st i = $1 holds
i * r = $1 * r;
reconsider rr = r as Integer ;
A1: 0. INT.Ring = 0 ;
A2: S₁[ 0 ] by A1, BINOM:12;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for i being Integer st i = n + 1 holds
i * r = (n + 1) * r

let i be Integer; :: thesis: ( i = n + 1 implies i * r = (n + 1) * r )
assume A5: i = n + 1 ; :: thesis: i * r = (n + 1) * r
reconsider Kn = n, K1 = 1 as Integer ;
reconsider n1 = 1 as Element of NAT ;
A6: K1 * r = n1 * r by BINOM:13;
thus i * r = (Kn * r) + (K1 * r) by A5
.= (n * r) + (n1 * r) by A4, A6
.= (n + 1) * r by BINOM:15 ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for n being Element of NAT
for i being Integer st i = n holds
i * r = n * r ; :: thesis: verum