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