let V be ComplexLinearSpace; :: thesis: 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 )
let v be VECTOR of V; :: thesis: 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 )
let L be C_Linear_Combination of V; :: thesis: ( L is convex & Carrier L = {v} implies ( ex r being Real st
( r = L . v & r = 1 ) & Sum L = (L . v) * v ) )
assume that
A1: L is convex and
A2: Carrier L = {v} ; :: thesis: ( ex r being Real st
( r = L . v & r = 1 ) & Sum L = (L . v) * v )
reconsider L = L as C_Linear_Combination of {v} by A2, Def3;
consider F being FinSequence of the carrier of V such that
A3: ( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) ) by A1, Def203;
consider f being FinSequence of REAL such that
A4: ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by A3;
card (Carrier L) = 1 by A2, CARD_1:50;
then len F = 1 by A3, FINSEQ_4:77;
then A5: dom f = Seg 1 by A4, FINSEQ_1:def 3;
then A6: 1 in dom f ;
then A7: f . 1 = L . (F . 1) by A4;
A8: f . 1 = f /. 1 by A6, PARTFUN1:def 8;
reconsider r = f /. 1 as Element of REAL ;
f = <*r*> by A5, A8, FINSEQ_1:def 8;
then A9: Sum f = r by FINSOP_1:12;
F = <*v*> by A2, A3, FINSEQ_3:106;
then r = L . v by A7, A8, FINSEQ_1:def 8;
hence ( ex r being Real st
( r = L . v & r = 1 ) & Sum L = (L . v) * v ) by A4, A9, Th50; :: thesis: verum