:: deftheorem defines zerovect MIDSP_1:def 16 :
for M being MidSp holds zerovect M = ID M;