for M being MidSp
for u, v, w being Vector of M st u + v = u + w holds
v = w