:: deftheorem Def17 defines LCAdd RLVECT_2:def 17 :
for V being RealLinearSpace
for b₂ being BinOp of (LinComb V) holds
( b₂ = LCAdd V iff for e1, e2 being Element of LinComb V holds b₂ . (e1,e2) = (@ e1) + (@ e2) );