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

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