:: deftheorem Def3 defines ZeroLC VECTSP_6:def 3 :
for GF being non empty ZeroStr
for V being non empty ModuleStr over GF
for b₃ being Linear_Combination of V holds
( b₃ = ZeroLC V iff Carrier b₃ = {} );