let V be ComplexLinearSpace; :: thesis: 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 )
let v be VECTOR of V; :: thesis: 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 )
let L be C_Linear_Combination of {v}; :: thesis: ( L is convex implies ( ex r being Real st
( r = L . v & r = 1 ) & Sum L = (L . v) * v ) )
Carrier L c= {v} by Def4;
then A1: ( Carrier L = {} or Carrier L = {v} ) by ZFMISC_1:33;
assume L is convex ; :: thesis: ( ex r being Real st
( r = L . v & r = 1 ) & Sum L = (L . v) * v )
hence ( ex r being Real st
( r = L . v & r = 1 ) & Sum L = (L . v) * v ) by A1, Th77, Th80; :: thesis: verum