theorem :: RLVECT_1:59

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