theorem Th2: :: ZMODUL01:2

for R being Ring
for V being LeftMod of R
for v being Vector of V holds - v = (- (1. R)) * v by VECTSP_1:14;