let a be Real; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for v being Element of V holds a * (- v) = (- a) * v
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for v being Element of V holds a * (- v) = (- a) * v
let v be Element of V; :: thesis: a * (- v) = (- a) * v
thus a * (- v) = a * ((- 1) * v) by Th16
.= (a * (- 1)) * v by Def7
.= (- a) * v ; :: thesis: verum