theorem :: ZMODUL01:7

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