:: deftheorem Def10 defines + RLVECT_2:def 10 :
for V being non empty addLoopStr
for L1, L2, b₄ being Linear_Combination of V holds
( b₄ = L1 + L2 iff for v being Element of V holds b₄ . v = (L1 . v) + (L2 . v) );