let V be RealLinearSpace; :: thesis: for M being non empty Subset of V ex L being Linear_Combination of M st L is convex
let M be non empty Subset of V; :: thesis: ex L being Linear_Combination of M st L is convex
consider u being set such that
A1: u in M by XBOOLE_0:def 1;
reconsider u = u as Element of V by A1;
consider L being Linear_Combination of {u} such that
A2: L . u = 1 from RLVECT_4:sch 2();
{u} c= M by A1, ZFMISC_1:37;
then reconsider L = L as Linear_Combination of M by RLVECT_2:33;
A3: L is convex

proof

take <*u*> ; :: according to CONVEX1:def 3 :: thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex b₁ being FinSequence of REAL st
( len b₁ = len <*u*> & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (<*u*> . b₂) & 0 <= b₁ . b₂ ) ) ) ) )
thus <*u*> is one-to-one by FINSEQ_3:102; :: thesis: ( rng <*u*> = Carrier L & ex b₁ being FinSequence of REAL st
( len b₁ = len <*u*> & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (<*u*> . b₂) & 0 <= b₁ . b₂ ) ) ) ) )
A4: Carrier L c= {u} by RLVECT_2:def 8;
u in { w where w is Element of V : L . w <> 0 } by A2;
then u in Carrier L by RLVECT_2:def 6;
then {u} c= Carrier L by ZFMISC_1:37;
hence Carrier L = {u} by A4, XBOOLE_0:def 10
.= rng <*u*> by FINSEQ_1:55 ;
:: thesis: ex b₁ being FinSequence of REAL st
( len b₁ = len <*u*> & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (<*u*> . b₂) & 0 <= b₁ . b₂ ) ) ) )
take f = <*rr*>; :: thesis: ( len f = len <*u*> & Sum f = 1 & ( for b₁ being set holds
( not b₁ in dom f or ( f . b₁ = L . (<*u*> . b₁) & 0 <= f . b₁ ) ) ) )
( len f = len <*u*> & Sum f = 1 & ( for n being Element of NAT st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )

proof

A5: len <*1*> = 1 by FINSEQ_1:56
.= len <*u*> by FINSEQ_1:56 ;
for n being Element of NAT st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 )

proof

let n be Element of NAT ; :: thesis: ( n in dom f implies ( f . n = L . (<*u*> . n) & f . n >= 0 ) )
assume n in dom f ; :: thesis: ( f . n = L . (<*u*> . n) & f . n >= 0 )
then n in {1} by FINSEQ_1:4, FINSEQ_1:55;
then A6: n = 1 by TARSKI:def 1;
then f . n = L . u by A2, FINSEQ_1:57
.= L . (<*u*> . n) by A6, FINSEQ_1:57 ;
hence ( f . n = L . (<*u*> . n) & f . n >= 0 ) by A6, FINSEQ_1:57; :: thesis: verum

end;

hence ( len f = len <*u*> & Sum f = 1 & ( for n being Element of NAT st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) by A5, FINSOP_1:12; :: thesis: verum

end;

hence ( len f = len <*u*> & Sum f = 1 & ( for b₁ being set holds
( not b₁ in dom f or ( f . b₁ = L . (<*u*> . b₁) & 0 <= f . b₁ ) ) ) ) ; :: thesis: verum

end;

take L ; :: thesis: L is convex
thus L is convex by A3; :: thesis: verum