let V be ComplexLinearSpace; :: thesis: for L being C_Linear_Combination of V st L is convex holds
Carrier L <> {}
let L be C_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
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 Def203;
assume Carrier L = {} ; :: thesis: contradiction
then len F = 0 by A3, CARD_1:47, FINSEQ_4:77;
hence contradiction by A3, FINSEQ_1:32, RVSUM_1:102; :: thesis: verum