theorem :: MIDSP_1:54

for M being MidSp holds the addF of (vectgroup M) = addvect M ;