let w, w1 be VECTOR of V; :: thesis: ( w + w = u + v & w1 + w1 = u + v implies w = w1 )
assume ( w + w = u + v & w1 + w1 = u + v ) ; :: thesis: w = w1
then 0. V = (w + w) - (w1 + w1) by RLVECT_1:15
.= w + (w - (w1 + w1)) by RLVECT_1:def 3
.= w + ((w - w1) - w1) by RLVECT_1:27
.= (w + (w - w1)) - w1 by RLVECT_1:def 3
.= (w - w1) + (w - w1) by RLVECT_1:def 3 ;
then w - w1 = 0. V by RLVECT_1:20;
hence w = w1 by RLVECT_1:21; :: thesis: verum