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) = (- (1 * a)) * v by Th24
.= ((- 1) * a) * v
.= (- 1) * (a * v) by Def7
.= - (a * v) by Th16 ; :: thesis: verum