theorem LMINTRNG2: :: ZMODUL06:14

for x, v being Element of INT.Ring
for v1 being Integer st v = v1 holds
(Int-mult-left INT.Ring) . (x,v) = x * v1