theorem :: RLVECT_1:29

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, u, w being Element of V holds v - (u - w) = (v - u) + w