theorem :: RLVECT_1:2

for V being non empty addMagma
for v, w being Element of V holds v + w = the addF of V . (v,w) ;