:: deftheorem Def13 defines + MIDSP_1:def 13 :
for M being MidSp
for u1, v1, b₄ being Element of setvect M holds
( b₄ = u1 + v1 iff for u, v being Vector of M st u1 = u & v1 = v holds
b₄ = u + v );