theorem Th46: :: RLVECT_1:46

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