theorem :: RLVECT_1:73

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