theorem :: RLVECT_1:23

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for w, v1, v2 being Element of V st w - v1 = w - v2 holds
v1 = v2