:: deftheorem Def15 defines complvect MIDSP_1:def 15 :
for M being MidSp
for b₂ being UnOp of (setvect M) holds
( b₂ = complvect M iff for W being Element of setvect M holds W + (b₂ . W) = ID M );