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 ;
then reconsider L = L as Linear_Combination of M by RLVECT_2:21;
take L ; :: thesis: L is convex
L is convex
proof
take <*u*> ; :: according to CONVEX1:def 3 :: thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) ) )

thus <*u*> is one-to-one by FINSEQ_3:93; :: thesis: ( rng <*u*> = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) ) )

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 ;
hence Carrier L = {u} by XBOOLE_0:def 10
.= rng <*u*> by FINSEQ_1:38 ;
:: thesis: ex b1 being FinSequence of REAL st
( len b1 = len <*u*> & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (<*u*> . b2) & 0 <= b1 . b2 ) ) ) )

take f = <*rr*>; :: thesis: ( len f = len <*u*> & Sum f = 1 & ( for b1 being set holds
( not b1 in dom f or ( f . b1 = L . (<*u*> . b1) & 0 <= f . b1 ) ) ) )

A3: for n being Element of NAT st n in dom f holds
( f . n = L . (<*u*> . n) & f . n >= 0 )
proof
let n be Element of 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 ;
then A4: n = 1 by TARSKI:def 1;
then f . n = L . u by
.= L . (<*u*> . n) by ;
hence ( f . n = L . (<*u*> . n) & f . n >= 0 ) ; :: thesis: verum
end;
len <*1*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39 ;
hence ( len f = len <*u*> & Sum f = 1 & ( for b1 being set holds
( not b1 in dom f or ( f . b1 = L . (<*u*> . b1) & 0 <= f . b1 ) ) ) ) by ; :: thesis: verum
end;
hence L is convex ; :: thesis: verum