theorem :: VECTSP_1:18

for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds
( (0. V) - v = - v & v - (0. V) = v ) by RLVECT_1:13, RLVECT_1:14;