let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V holds (- u) + (- v) = - (u + v)
let u, v be VECTOR of V; :: thesis: (- u) + (- v) = - (u + v)
(u + v) + ((- u) + (- v)) = ((u + v) + (- u)) + (- v) by RLVECT_1:def 3
.= (v + (u + (- u))) + (- v) by RLVECT_1:def 3
.= (v + (0. V)) + (- v) by RLVECT_1:5
.= v + (- v) by RLVECT_1:4
.= 0. V by RLVECT_1:5 ;
hence (- u) + (- v) = - (u + v) by RLVECT_1:def 10; :: thesis: verum