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:28
.= w + (w - (w1 + w1)) by RLVECT_1:def 6
.= w + ((w - w1) - w1) by RLVECT_1:41
.= (w + (w - w1)) - w1 by RLVECT_1:def 6
.= (w - w1) + (w - w1) by RLVECT_1:def 6 ;
then w - w1 = 0. V by RLVECT_1:34;
hence w = w1 by RLVECT_1:35; :: thesis: verum