:: deftheorem Def5 defines ZeroLC RLVECT_2:def 5 :
for V being non empty addLoopStr
for b₂ being Linear_Combination of V holds
( b₂ = ZeroLC V iff Carrier b₂ = {} );