let a be real number ; :: thesis: for V being RealLinearSpace
for v being VECTOR of V holds a * (- v) = (- a) * v
let V be RealLinearSpace; :: thesis: for v being VECTOR of V holds a * (- v) = (- a) * v
let v be VECTOR of V; :: thesis: a * (- v) = (- a) * v
thus a * (- v) = a * ((- 1) * v) by Th29
.= (a * (- 1)) * v by Def10
.= (- a) * v ; :: thesis: verum