for V being non empty addLoopStr
for l being C_Linear_Combination of {} the carrier of V holds l = ZeroCLC V