:: deftheorem Def3 defines Linear_Combination RLVECT_2:def 3 :
for V being non empty ZeroStr
for b₂ being Element of Funcs ( the carrier of V,REAL) holds
( b₂ is Linear_Combination of V iff ex T being finite Subset of V st
for v being Element of V st not v in T holds
b₂ . v = 0 );