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