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 Th38
.= ((- 1) * a) * v
.= (- 1) * (a * v) by Def9
.= - (a * v) by Th29 ; :: thesis: verum