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 = jj by RLVECT_4:37;
consider F being FinSequence of the carrier of V such that
A2: ( F is one-to-one & rng F = Carrier L ) and
Sum L = Sum (L (#) F) by RLVECT_2:def 8;
v in Carrier L by A1, RLVECT_2:19;
then ( Carrier L c= {v} & {v} c= Carrier L ) by RLVECT_2:def 6, ZFMISC_1:31;
then A3: {v} = Carrier L by XBOOLE_0:def 10;
then F = <*v*> by A2, FINSEQ_3:97;
then A4: F . 1 = v by FINSEQ_1:def 8;
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: 1 in REAL by XREAL_0:def 1;
A7: len F = 1 by A3, A2, FINSEQ_3:96;
then 1 in dom f by A5, FINSEQ_3:25;
then A8: f . 1 = L . (F . 1) by A5;
then f = <*1*> by A1, A5, A7, A4, FINSEQ_1:40;
then rng f = {1} by FINSEQ_1:38;
then rng f c= REAL by ZFMISC_1:31, A6;
then reconsider f = f as FinSequence of REAL by FINSEQ_1:def 4;
A9: 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, A7, A8, A4, A10, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;

f = <*1*> by A1, A5, A7, A8, A4, FINSEQ_1:40;
then Sum f = jj by FINSOP_1:11;
then reconsider L = L as Convex_Combination of V by A2, 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 by A3, RLVECT_2:def 6, ZFMISC_1:31;
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:35;
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 8; :: thesis: verum