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

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