theorem Th6: :: RLAFFIN1:6

for V being non empty Abelian right_zeroed addLoopStr
for A being Subset of V holds (0. V) + A = A