theorem :: RLVECT_1:7

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