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:47
.= (a * (v - u)) - (a * (v - u)) by RLVECT_1:39
.= 0. V by RLVECT_1:28 ;
hence a * (u - v) = - (a * (v - u)) by RLVECT_1:def 11; :: thesis: verum