:: deftheorem Def8 defines + CONVEX4:def 8 :
for V being non empty addLoopStr
for L1, L2, b₄ being C_Linear_Combination of V holds
( b₄ = L1 + L2 iff for v being Element of V holds b₄ . v = (L1 . v) + (L2 . v) );