:: deftheorem Def8 defines vect MIDSP_2:def 8 :
for M being MidSp
for b₂ being Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M) holds
( b₂ = vect M iff for p, q being Point of M holds b₂ . (p,q) = vect (p,q) );