:: deftheorem Def14 defines addvect MIDSP_1:def 14 :
for M being MidSp
for b₂ being BinOp of (setvect M) holds
( b₂ = addvect M iff for u1, v1 being Element of setvect M holds b₂ . (u1,v1) = u1 + v1 );