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;

(L * F) . n = L . x by A5, A6, A7, FUNCT_1:12;

hence contradiction by A3, A4, A5, A7, A8, MATRPROB:5; :: thesis: verum

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

reconsider n = n as Nat by A5;(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;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

(L * F) . n = L . x by A5, A6, A7, FUNCT_1:12;

hence contradiction by A3, A4, A5, A7, A8, MATRPROB:5; :: thesis: verum