theorem Th15: :: MIDSP_2:15

for M being MidSp holds
( ( for a being set holds
( a is Element of (vectgroup M) iff a is Vector of M ) ) & 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )