for V being non empty addLoopStr
for L being C_Linear_Combination of V
for v being Element of V holds
( L . v = 0c iff not v in Carrier L )