let a be Real; :: 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 RLVECT_1:25
.= (- a) * v by RLVECT_1:24 ; :: thesis: verum