theorem Th2: :: ZMODUL01:2
for V being Z_Module
for v being Vector of V holds - v = (- (1. INT.Ring)) * v by VECTSP_1:14;