let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V st L is convex holds
Carrier L <> {}
let L be Linear_Combination of V; :: thesis: ( L is convex implies Carrier L <> {} )
assume L is convex ; :: thesis: Carrier L <> {}
then consider F being FinSequence of the carrier of V such that
A1: ( F is one-to-one & rng F = Carrier L ) and
A2: 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 ) ) ) ;
consider f being FinSequence of REAL such that
A3: ( 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 A2;
assume Carrier L = {} ; :: thesis: contradiction
then len F = 0 by A1, CARD_1:27, FINSEQ_4:62;
then f = <*> REAL by A3;
hence contradiction by A3, RVSUM_1:72; :: thesis: verum