let x be set ; :: thesis: for V being RealLinearSpace
for L being Linear_Combination of V st L is convex holds
L . x <= 1
let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V st L is convex holds
L . x <= 1
let L be Linear_Combination of V; :: thesis: ( L is convex implies L . x <= 1 )
assume A1: L is convex ; :: thesis: L . x <= 1
then sum L = 1 by Th62;
then consider F being FinSequence of V such that
F is one-to-one and
A2: rng F = Carrier L and
A3: 1 = Sum (L * F) by Def3;
assume A4: L . x > 1 ; :: thesis: contradiction
then x in dom L by FUNCT_1:def 2;
then reconsider v = x as Element of V by FUNCT_2:def 1;
v in Carrier L by A4;
then consider n being object such that
A5: n in dom F and
A6: F . n = v by A2, FUNCT_1:def 3;
len (L * F) = len F by FINSEQ_2:33;
then A7: dom (L * F) = dom F by FINSEQ_3:29;
A8: now :: thesis: for i being Nat st i in dom (L * F) holds
(L * F) . i >= 0
let i be Nat; :: thesis: ( i in dom (L * F) implies (L * F) . i >= 0 )
assume i in dom (L * F) ; :: thesis: (L * F) . i >= 0
then ( (L * F) . i = L . (F . i) & F . i = F /. i ) by A7, FUNCT_1:12, PARTFUN1:def 6;
hence (L * F) . i >= 0 by A1, Th62; :: thesis: verum
end;
reconsider n = n as Nat by A5;
(L * F) . n = L . x by A5, A6, A7, FUNCT_1:12;
hence contradiction by A3, A4, A5, A7, A8, MATRPROB:5; :: thesis: verum