theorem :: MIDSP_1:38

for M being MidSp
for b being Element of M holds ID M = vect (b,b) by Th32;