theorem :: CONVEX4:86

for V being ComplexLinearSpace
for v being VECTOR of V
for L being C_Linear_Combination of {v} st L is convex holds
( ex r being Real st
( r = L . v & r = 1 ) & Sum L = (L . v) * v )