set u = the Element of V;
consider L being Linear_Combination of { the Element of V} such that
A1: L . the Element of V = jj by RLVECT_4:37;
reconsider L = L as Linear_Combination of V ;
take L ; :: thesis: L is convex
L is convex

proof

take <* the Element of V*> ; :: according to CONVEX1:def 3 :: thesis: ( <* the Element of V*> is one-to-one & rng <* the Element of V*> = Carrier L & ex b₁ being FinSequence of REAL st
( len b₁ = len <* the Element of V*> & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (<* the Element of V*> . b₂) & 0 <= b₁ . b₂ ) ) ) ) )
thus <* the Element of V*> is one-to-one by FINSEQ_3:93; :: thesis: ( rng <* the Element of V*> = Carrier L & ex b₁ being FinSequence of REAL st
( len b₁ = len <* the Element of V*> & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (<* the Element of V*> . b₂) & 0 <= b₁ . b₂ ) ) ) ) )
the Element of V in { w where w is Element of V : L . w <> 0 } by A1;
then the Element of V in Carrier L by RLVECT_2:def 4;
then ( Carrier L c= { the Element of V} & { the Element of V} c= Carrier L ) by RLVECT_2:def 6, ZFMISC_1:31;
hence Carrier L = { the Element of V} by XBOOLE_0:def 10
.= rng <* the Element of V*> by FINSEQ_1:38 ;
:: thesis: ex b₁ being FinSequence of REAL st
( len b₁ = len <* the Element of V*> & Sum b₁ = 1 & ( for b₂ being set holds
( not b₂ in dom b₁ or ( b₁ . b₂ = L . (<* the Element of V*> . b₂) & 0 <= b₁ . b₂ ) ) ) )
take f = <*rr*>; :: thesis: ( len f = len <* the Element of V*> & Sum f = 1 & ( for b₁ being set holds
( not b₁ in dom f or ( f . b₁ = L . (<* the Element of V*> . b₁) & 0 <= f . b₁ ) ) ) )
A2: for n being Element of NAT st n in dom f holds
( f . n = L . (<* the Element of V*> . n) & f . n >= 0 )

proof

let n be Element of NAT ; :: thesis: ( n in dom f implies ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) )
assume n in dom f ; :: thesis: ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 )
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then A3: n = 1 by TARSKI:def 1;
then f . n = L . the Element of V by A1
.= L . (<* the Element of V*> . n) by A3 ;
hence ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ; :: thesis: verum

end;

len <*1*> = 1 by FINSEQ_1:39
.= len <* the Element of V*> by FINSEQ_1:39 ;
hence ( len f = len <* the Element of V*> & Sum f = 1 & ( for b₁ being set holds
( not b₁ in dom f or ( f . b₁ = L . (<* the Element of V*> . b₁) & 0 <= f . b₁ ) ) ) ) by A2, FINSOP_1:11; :: thesis: verum

end;

hence L is convex ; :: thesis: verum