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

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