theorem Th3: :: RLVECT_4:3

for a being Real
for V being RealLinearSpace
for v being VECTOR of V holds - (a * v) = (- a) * v