let V be RealLinearSpace; :: thesis: for w, v, u being VECTOR of V holds (w - v) + (v - u) = w - u
let w, v, u be VECTOR of V; :: thesis: (w - v) + (v - u) = w - u
thus (w - v) + (v - u) = w - (v - (v - u)) by RLVECT_1:29
.= w - ((v - v) + u) by RLVECT_1:29
.= w - ((0. V) + u) by RLVECT_1:15
.= w - u by RLVECT_1:4 ; :: thesis: verum