theorem Th65: :: RLVECT_1:66

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