theorem Th45: :: MIDSP_1:45
for M being MidSp
for u being Vector of M ex v being Vector of M st u + v = ID M