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