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 6
.= (v + (u + (- u))) + (- v) by RLVECT_1:def 6
.= (v + (0. V)) + (- v) by RLVECT_1:16
.= v + (- v) by RLVECT_1:10
.= 0. V by RLVECT_1:16 ;
hence (- u) + (- v) = - (u + v) by RLVECT_1:def 11; :: thesis: verum