:: deftheorem Def9 defines + RMOD_4:def 9 :
for R being Ring
for V being RightMod of R
for L1, L2, b₅ being Linear_Combination of V holds
( b₅ = L1 + L2 iff for v being Vector of V holds b₅ . v = (L1 . v) + (L2 . v) );