theorem :: RLVECT_1:63

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