theorem :: RLVECT_1:22

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, v being Element of V ex w being Element of V st v - w = u