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 & 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, Def4;
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;
len F = 0 by A2, A3, CARD_1:47, FINSEQ_4:77;
hence contradiction by A4, FINSEQ_1:32, RVSUM_1:102; :: thesis: verum