theorem :: ZMODUL01:151

for R being non empty addLoopStr
for a being Element of R
for i being Element of INT.Ring
for i1 being Element of NAT st i = i1 holds
(Int-mult-left R) . (i,a) = i1 * a by Def23;