:: deftheorem defines vectgroup MIDSP_1:def 17 :
for M being MidSp holds vectgroup M = addLoopStr(# (setvect M),(addvect M),(zerovect M) #);