theorem Th8: :: ZMODUL01:8

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