for V being ComplexLinearSpace
for L being C_Linear_Combination of V st L is convex holds
L <> ZeroCLC V