theorem Th80: :: CONVEX4:83

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