:: deftheorem Def2 defines Linear_Combination RMOD_4:def 2 :
for R being Ring
for V being RightMod of R
for b₃ being Element of Funcs ( the carrier of V, the carrier of R) holds
( b₃ is Linear_Combination of V iff ex T being finite Subset of V st
for v being Vector of V st not v in T holds
b₃ . v = 0. R );