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

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

hence
L is convex
; :: thesis: verum
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_{1} being FinSequence of REAL st

( len b_{1} = len <* the Element of V*> & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (<* the Element of V*> . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) ) )

thus <* the Element of V*> is one-to-one by FINSEQ_3:93; :: thesis: ( rng <* the Element of V*> = Carrier L & ex b_{1} being FinSequence of REAL st

( len b_{1} = len <* the Element of V*> & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (<* the Element of V*> . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) ) )

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_{1} being FinSequence of REAL st

( len b_{1} = len <* the Element of V*> & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (<* the Element of V*> . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) )

take f = <*rr*>; :: thesis: ( len f = len <* the Element of V*> & Sum f = 1 & ( for b_{1} being set holds

( not b_{1} in dom f or ( f . b_{1} = L . (<* the Element of V*> . b_{1}) & 0 <= f . b_{1} ) ) ) )

A2: for n being Element of NAT st n in dom f holds

( f . n = L . (<* the Element of V*> . n) & f . n >= 0 )

.= len <* the Element of V*> by FINSEQ_1:39 ;

hence ( len f = len <* the Element of V*> & Sum f = 1 & ( for b_{1} being set holds

( not b_{1} in dom f or ( f . b_{1} = L . (<* the Element of V*> . b_{1}) & 0 <= f . b_{1} ) ) ) )
by A2, FINSOP_1:11; :: thesis: verum

end;( len b

( not b

thus <* the Element of V*> is one-to-one by FINSEQ_3:93; :: thesis: ( rng <* the Element of V*> = Carrier L & ex b

( len b

( not 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

( len b

( not b

take f = <*rr*>; :: thesis: ( len f = len <* the Element of V*> & Sum f = 1 & ( for b

( not 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

len <*1*> =
1
by FINSEQ_1:39
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, FINSEQ_1:40

.= L . (<* the Element of V*> . n) by A3, FINSEQ_1:40 ;

hence ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ; :: thesis: verum

end;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, FINSEQ_1:40

.= L . (<* the Element of V*> . n) by A3, FINSEQ_1:40 ;

hence ( f . n = L . (<* the Element of V*> . n) & f . n >= 0 ) ; :: thesis: verum

.= len <* the Element of V*> by FINSEQ_1:39 ;

hence ( len f = len <* the Element of V*> & Sum f = 1 & ( for b

( not b