let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V
for v being VECTOR of V st L is circled & L . v <= 0 holds
not v in Carrier L
let L be Linear_Combination of V; :: thesis: for v being VECTOR of V st L is circled & L . v <= 0 holds
not v in Carrier L
let v be VECTOR of V; :: thesis: ( L is circled & L . v <= 0 implies not v in Carrier L )
assume that
A1: L is circled and
A2: L . v <= 0 ; :: thesis: not v in Carrier L

per cases ( L . v = 0 or L . v < 0 ) by A2;

suppose L . v = 0 ; :: thesis: not v in Carrier L

hence not v in Carrier L by RLVECT_2:28; :: thesis: verum

end;

suppose A3: L . v < 0 ; :: thesis: not v in Carrier L

now

assume A4: v in Carrier L ; :: thesis: contradiction
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A5: rng F = Carrier L and
A6: 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
A7: len f = len F and
Sum f = 1 and
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) by A6;
consider n being set such that
A9: ( n in dom F & F . n = v ) by A4, A5, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A9;
n in Seg (len F) by A9, FINSEQ_1:def 3;
then A10: n in dom f by A7, FINSEQ_1:def 3;
then L . v = f . n by A8, A9;
hence contradiction by A3, A8, A10; :: thesis: verum

end;

hence not v in Carrier L ; :: thesis: verum

end;

end;