consider u being object such that
A1: u in M by XBOOLE_0:def 1;
reconsider u = u as Element of V by A1;
consider L being Linear_Combination of {u} such that
A2: L . u = jj by RLVECT_4:37;
{u} c= M by A1, ZFMISC_1:31;
then reconsider L = L as Linear_Combination of M by RLVECT_2:21;
take L ; :: thesis: L is circled
L is circled

proof

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 ) ) ) )
A3: 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 = <*jj*> as FinSequence of REAL ;
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 ) ) )
A4: 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:2, FINSEQ_1:38;
then A5: n = 1 by TARSKI:def 1;
thus ( f . n = L . (<*u*> . n) & f . n >= 0 ) by A2, A5; :: thesis: verum

end;

len <*jj*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39 ;
hence ( 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, FINSOP_1:11; :: thesis: verum

end;

u in { w where w is Element of V : L . w <> 0 } by A2;
then u in Carrier L by RLVECT_2:def 4;
then ( Carrier L c= {u} & {u} c= Carrier L ) by RLVECT_2:def 6, ZFMISC_1:31;
then Carrier L = {u} ;
hence ( <*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 A3, FINSEQ_1:38, FINSEQ_3:93; :: thesis: verum

end;

hence L is circled ; :: thesis: verum