let V be RealLinearSpace; :: thesis: for o being Element of V
for a being Real holds - (a * o) = (- a) * o
let o be Element of V; :: thesis: for a being Real holds - (a * o) = (- a) * o
let a be Real; :: thesis: - (a * o) = (- a) * o
thus - (a * o) = a * (- o) by RLVECT_1:25
.= (- a) * o by RLVECT_1:24 ; :: thesis: verum