theorem Th81: :: CONVEX4:84

for V being ComplexLinearSpace
for v1, v2 being VECTOR of V
for L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds
( ex r1, r2 being Real st
( r1 = L . v1 & r2 = L . v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) & Sum L = ((L . v1) * v1) + ((L . v2) * v2) )