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_{1}[ 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_{1}[ 0 ]
by A1, BINOM:12;

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[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

for i being Integer st i = n holds

i * r = n * r

defpred S

i * r = $1 * r;

reconsider rr = r as Integer ;

A1: 0. INT.Ring = 0 ;

A2: S

A3: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A4: S

now :: thesis: for i being Integer st i = n + 1 holds

i * r = (n + 1) * r

hence
Si * 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;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

hence for n being Element of NAT

for i being Integer st i = n holds

i * r = n * r ; :: thesis: verum