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 ; :: thesis: verum