let V be RealLinearSpace; :: thesis: ex L being Linear_Combination of V st L is circled
consider u being Element of V;
consider L being Linear_Combination of {u} such that
A1: L . u = 1 from RLVECT_4:sch 2();
A2: L is circled

proof

A3: Carrier L c= {u} by RLVECT_2:def 8;
u in { w where w is Element of V : L . w <> 0 } by A1;
then u in Carrier L by RLVECT_2:def 6;
then {u} c= Carrier L by ZFMISC_1:37;
then A4: Carrier L = {u} by A3, XBOOLE_0:def 10;
A5: ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )

proof

reconsider f = <*1*> as FinSequence of REAL ;
A6: len <*1*> = 1 by FINSEQ_1:56
.= len <*u*> by FINSEQ_1:56 ;
A7: for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 )

proof

let n be 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 A8: n = 1 by TARSKI:def 1;
then f . n = L . u by A1, FINSEQ_1:57
.= L . (<*u*> . n) by A8, FINSEQ_1:57 ;
hence ( f . n = L . (<*u*> . n) & f . n >= 0 ) by A8, FINSEQ_1:57; :: thesis: verum

end;

take f ; :: thesis: ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) )
thus ( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) by A6, A7, FINSOP_1:12; :: thesis: verum

end;

take <*u*> ; :: according to CIRCLED1:def 4 :: thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) )
thus ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex f being FinSequence of REAL st
( len f = len <*u*> & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 ) ) ) ) by A4, A5, FINSEQ_1:55, FINSEQ_3:102; :: thesis: verum

end;

take L ; :: thesis: L is circled
thus L is circled by A2; :: thesis: verum