theorem Th4: :: RLVECT_1:4

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( v + (0. V) = v & (0. V) + v = v )