:: deftheorem Def15 defines C_LCAdd CONVEX4:def 15 :
for V being non empty CLSStruct
for b₂ being BinOp of (C_LinComb V) holds
( b₂ = C_LCAdd V iff for e1, e2 being Element of C_LinComb V holds b₂ . (e1,e2) = (@ e1) + (@ e2) );