let V be RealLinearSpace; :: thesis: for v being VECTOR of V ex L being Convex_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is Convex_Combination of A ) )
let v be VECTOR of V; :: thesis: ex L being Convex_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is Convex_Combination of A ) )
consider L being Linear_Combination of {v} such that
A1: L . v = 1 from RLVECT_4:sch 2();
A2: Carrier L c= {v} by RLVECT_2:def 8;
v in Carrier L by A1, RLVECT_2:28;
then {v} c= Carrier L by ZFMISC_1:37;
then A3: {v} = Carrier L by A2, XBOOLE_0:def 10;
consider F being FinSequence of the carrier of V such that
A4: ( F is one-to-one & rng F = Carrier L & Sum L = Sum (L (#) F) ) by RLVECT_2:def 10;
deffunc H₁( set ) -> set = L . (F . $1);
consider f being FinSequence such that
A5: ( len f = len F & ( for n being Nat st n in dom f holds
f . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A6: len F = 1 by A3, A4, FINSEQ_3:105;
then 1 in dom f by A5, FINSEQ_3:27;
then A7: f . 1 = L . (F . 1) by A5;
F = <*v*> by A3, A4, FINSEQ_3:106;
then A8: F . 1 = v by FINSEQ_1:def 8;
rng f c= REAL

proof

f = <*1*> by A1, A5, A6, A7, A8, FINSEQ_1:57;
then rng f = {1} by FINSEQ_1:55;
hence rng f c= REAL by ZFMISC_1:37; :: thesis: verum

end;

then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
f = <*1*> by A1, A5, A6, A7, A8, FINSEQ_1:57;
then A9: Sum f = 1 by FINSOP_1:12;
for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )

proof

let n be Nat; :: thesis: ( n in dom f implies ( f . n = L . (F . n) & f . n >= 0 ) )
assume A10: n in dom f ; :: thesis: ( f . n = L . (F . n) & f . n >= 0 )
then n in Seg (len f) by FINSEQ_1:def 3;
hence ( f . n = L . (F . n) & f . n >= 0 ) by A1, A5, A6, A7, A8, A10, FINSEQ_1:4, TARSKI:def 1; :: thesis: verum

end;

then reconsider L = L as Convex_Combination of V by A4, A5, A9, CONVEX1:def 3;
A11: for A being non empty Subset of V st v in A holds
L is Convex_Combination of A

proof

let A be non empty Subset of V; :: thesis: ( v in A implies L is Convex_Combination of A )
assume v in A ; :: thesis: L is Convex_Combination of A
then {v} c= A by ZFMISC_1:37;
hence L is Convex_Combination of A by A3, RLVECT_2:def 8; :: thesis: verum

end;

take L ; :: thesis: ( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is Convex_Combination of A ) )
Sum L = 1 * v by A1, A3, RLVECT_2:53;
hence ( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is Convex_Combination of A ) ) by A11, RLVECT_1:def 9; :: thesis: verum