:: deftheorem defines Carrier VECTSP_6:def 2 :
for GF being non empty ZeroStr
for V being non empty ModuleStr over GF
for L being Linear_Combination of V holds Carrier L = { v where v is Element of V : L . v <> 0. GF } ;