for M being MidSp
for u being Vector of M holds u + (ID M) = u