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 convex

L is convex

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 convex

L is convex

proof

hence
L is convex
; :: thesis: verum
take
<*u*>
; :: according to CONVEX1:def 3 :: thesis: ( <*u*> is one-to-one & rng <*u*> = Carrier L & ex b_{1} being FinSequence of REAL st

( len b_{1} = len <*u*> & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (<*u*> . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) ) )

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

( len b_{1} = len <*u*> & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (<*u*> . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) ) )

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;

hence Carrier L = {u} by XBOOLE_0:def 10

.= rng <*u*> by FINSEQ_1:38 ;

:: thesis: ex b_{1} being FinSequence of REAL st

( len b_{1} = len <*u*> & Sum b_{1} = 1 & ( for b_{2} being set holds

( not b_{2} in dom b_{1} or ( b_{1} . b_{2} = L . (<*u*> . b_{2}) & 0 <= b_{1} . b_{2} ) ) ) )

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

( not b_{1} in dom f or ( f . b_{1} = L . (<*u*> . b_{1}) & 0 <= f . b_{1} ) ) ) )

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

( f . n = L . (<*u*> . n) & f . n >= 0 )

.= len <*u*> by FINSEQ_1:39 ;

hence ( len f = len <*u*> & Sum f = 1 & ( for b_{1} being set holds

( not b_{1} in dom f or ( f . b_{1} = L . (<*u*> . b_{1}) & 0 <= f . b_{1} ) ) ) )
by A3, FINSOP_1:11; :: thesis: verum

end;( len b

( not b

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

( len b

( not b

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;

hence Carrier L = {u} by XBOOLE_0:def 10

.= rng <*u*> by FINSEQ_1:38 ;

:: thesis: ex b

( len b

( not b

take f = <*rr*>; :: thesis: ( len f = len <*u*> & Sum f = 1 & ( for b

( not b

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

( f . n = L . (<*u*> . 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 . (<*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 A4: n = 1 by TARSKI:def 1;

then f . n = L . u by A2, FINSEQ_1:40

.= L . (<*u*> . n) by A4, FINSEQ_1:40 ;

hence ( f . n = L . (<*u*> . n) & f . n >= 0 ) ; :: thesis: verum

end;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 A4: n = 1 by TARSKI:def 1;

then f . n = L . u by A2, FINSEQ_1:40

.= L . (<*u*> . n) by A4, FINSEQ_1:40 ;

hence ( f . n = L . (<*u*> . n) & f . n >= 0 ) ; :: thesis: verum

.= len <*u*> by FINSEQ_1:39 ;

hence ( len f = len <*u*> & Sum f = 1 & ( for b

( not b