let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V
for a being Real holds a * (u - v) = - (a * (v - u))
let u, v be VECTOR of V; :: thesis: for a being Real holds a * (u - v) = - (a * (v - u))
let a be Real; :: thesis: a * (u - v) = - (a * (v - u))
(a * (v - u)) + (a * (u - v)) = (a * (v - u)) + (a * (- (v - u))) by RLVECT_1:33
.= (a * (v - u)) - (a * (v - u)) by RLVECT_1:25
.= 0. V by RLVECT_1:15 ;
hence a * (u - v) = - (a * (v - u)) by RLVECT_1:def 10; :: thesis: verum