theorem :: RLVECT_1:44

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds Sum <*v*> = v by Lm6;