let V be RealLinearSpace; :: thesis:
let v be VECTOR of V; :: thesis:
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 ;
then F = <*v*> by A2, FINSEQ_3:97;
then A4: F . 1 = v ;
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, A2, FINSEQ_3:96;
then 1 in dom f by A5, FINSEQ_3:25;
then A7: f . 1 = L . (F . 1) by A5;
then f = <*jj*> by A1, A5, A6, A4, FINSEQ_1:40;
then reconsider f = f as FinSequence of REAL ;
A8: for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )

proof

let n be Nat; :: thesis:
assume A9: n in dom f ; :: thesis:
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, A4, A9, FINSEQ_1:2, TARSKI:def 1; :: thesis:

end;

f = <*jj*> by A1, A5, A6, A7, A4, FINSEQ_1:40;
then Sum f = 1 by FINSOP_1:11;
then reconsider L = L as circled_Combination of V by A2, A5, A8, Def4;
A10: for A being non empty Subset of V st v in A holds
L is circled_Combination of A by ZFMISC_1:31, A3, RLVECT_2:def 6;
take L ; :: thesis:
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 circled_Combination of A ) ) by A10, RLVECT_1:def 8; :: thesis: