let V be RealLinearSpace; for v being VECTOR of V ex L being circled_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_Combination of A ) )
let v be VECTOR of V; ex L being circled_Combination of V st
( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_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
;
then
F = <*v*>
by A2, FINSEQ_3:97;
then A4:
F . 1 = v
by FINSEQ_1:def 8;
deffunc H1( 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 = H1(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 )
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
; ( Sum L = v & ( for A being non empty Subset of V st v in A holds
L is circled_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 circled_Combination of A ) )
by A10, RLVECT_1:def 8; verum