theorem Th9: :: ZMODUL01:9

for V being Z_Module
for a, b being Element of INT.Ring
for v being Vector of V holds (a - b) * v = (a * v) - (b * v)