theorem Th6: :: ZMODUL01:6
for V being Z_Module
for a being Element of INT.Ring
for v being Vector of V holds a * (- v) = - (a * v)