set G = vectgroup M;
( ( for x being Element of (vectgroup M) ex y being Element of (vectgroup M) st Double y = x ) & ( for x being Element of (vectgroup M) st Double x = 0. (vectgroup M) holds
x = 0. (vectgroup M) ) ) by Lm1;
hence vectgroup M is midpoint_operator by Def5; :: thesis: verum