theorem :: RLVECT_2:11

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v1, v2, v3 being Element of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3