:: deftheorem Def4 defines Linear_Combination VECTSP_6:def 4 :
for GF being non empty ZeroStr
for V being non empty ModuleStr over GF
for A being Subset of V
for b₄ being Linear_Combination of V holds
( b₄ is Linear_Combination of A iff Carrier b₄ c= A );