theorem LMINTRNG1: :: ZMODUL06:13

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