for M being MidSp
for a, b being Element of M holds (vect (a,(a @ b))) + (vect (a,(a @ b))) = vect (a,b)