theorem :: RLVECT_1:55

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V holds Sum <*v,w*> = (Sum <*v*>) + (Sum <*w*>)