let V be RealLinearSpace; :: thesis: for M being Subset of V st ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) holds
M is convex

let M be Subset of V; :: thesis: ( ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) implies M is convex )

assume A1: for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ; :: thesis: M is convex
let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for b1 being object holds
( b1 <= 0 or 1 <= b1 or not u in M or not v in M or (b1 * u) + ((1 - b1) * v) in M )

let rr be Real; :: thesis: ( rr <= 0 or 1 <= rr or not u in M or not v in M or (rr * u) + ((1 - rr) * v) in M )
reconsider r = rr as Real ;
assume that
A2: 0 < rr and
A3: rr < 1 and
A4: ( u in M & v in M ) ; :: thesis: (rr * u) + ((1 - rr) * v) in M
set N = {u,v};
A5: {u,v} c= M by ;
reconsider N = {u,v} as Subset of V ;
now :: thesis: (rr * u) + ((1 - rr) * v) in M
per cases ( u <> v or u = v ) ;
suppose A6: u <> v ; :: thesis: (rr * u) + ((1 - rr) * v) in M
consider L being Linear_Combination of {u,v} such that
A7: ( L . u = r & L . v = 1 - r ) by ;
reconsider L = L as Linear_Combination of N ;
A8: L is convex
proof
A9: r - r < 1 - r by ;
then v in { w where w is Element of V : L . w <> 0 } by A7;
then A10: v in Carrier L by RLVECT_2:def 4;
A11: for n being Element of NAT st n in dom <*r,(1 - r)*> holds
( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
proof
let n be Element of NAT ; :: thesis: ( n in dom <*r,(1 - r)*> implies ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) )
assume n in dom <*r,(1 - r)*> ; :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
then n in Seg (len <*r,(1 - r)*>) by FINSEQ_1:def 3;
then A12: n in {1,2} by ;
now :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
per cases ( n = 1 or n = 2 ) by ;
suppose A13: n = 1 ; :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
then L . (<*u,v*> . n) = r by ;
hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) by ; :: thesis: verum
end;
suppose A14: n = 2 ; :: thesis: ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 )
then L . (<*u,v*> . n) = 1 - r by ;
hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) by ; :: thesis: verum
end;
end;
end;
hence ( <*r,(1 - r)*> . n = L . (<*u,v*> . n) & <*r,(1 - r)*> . n >= 0 ) ; :: thesis: verum
end;
u in { w where w is Element of V : L . w <> 0 } by A2, A7;
then u in Carrier L by RLVECT_2:def 4;
then A15: ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by ;
take F = <*u,v*>; :: according to CONVEX1:def 3 :: thesis: ( F is one-to-one & rng F = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) ) )

A16: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:77
.= 1 ;
thus F is one-to-one by ; :: thesis: ( rng F = Carrier L & ex b1 being FinSequence of REAL st
( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) ) )

thus rng F = () \/ () by FINSEQ_1:31
.= {u} \/ () by FINSEQ_1:38
.= {u} \/ {v} by FINSEQ_1:38
.= {u,v} by ENUMSET1:1
.= Carrier L by ; :: thesis: ex b1 being FinSequence of REAL st
( len b1 = len F & Sum b1 = 1 & ( for b2 being set holds
( not b2 in dom b1 or ( b1 . b2 = L . (F . b2) & 0 <= b1 . b2 ) ) ) )

reconsider r = r as Element of REAL by XREAL_0:def 1;
reconsider jr = 1 - r as Element of REAL by XREAL_0:def 1;
take f = <*r,jr*>; :: thesis: ( len f = len F & Sum f = 1 & ( for b1 being set holds
( not b1 in dom f or ( f . b1 = L . (F . b1) & 0 <= f . b1 ) ) ) )

len <*r,(1 - r)*> = 2 by FINSEQ_1:44
.= len <*u,v*> by FINSEQ_1:44 ;
hence ( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) by ; :: thesis: verum
end;
Sum L = (r * u) + ((1 - r) * v) by ;
hence (rr * u) + ((1 - rr) * v) in M by A1, A5, A8; :: thesis: verum
end;
suppose A17: u = v ; :: thesis: (rr * u) + ((1 - rr) * v) in M
consider L being Linear_Combination of {u} such that
A18: L . u = jj by RLVECT_4:37;
reconsider L = L as Linear_Combination of N by ;
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = Carrier L & ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) ) )
proof
take <*u*> ; :: 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 ) ) ) )

A19: 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
take <*rr*> ; :: thesis: ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) )

A20: for n being Element of NAT st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )
proof
let n be Element of NAT ; :: thesis: ( n in dom <*rr*> implies ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) )
assume n in dom <*rr*> ; :: thesis: ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 )
then n in {1} by ;
then A21: n = 1 by TARSKI:def 1;
then <*rr*> . n = 1 by FINSEQ_1:40
.= L . (<*u*> . n) by ;
hence ( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ; :: thesis: verum
end;
len <*1*> = 1 by FINSEQ_1:39
.= len <*u*> by FINSEQ_1:39 ;
hence ( len <*rr*> = len <*u*> & Sum <*rr*> = 1 & ( for n being Nat st n in dom <*rr*> holds
( <*rr*> . n = L . (<*u*> . n) & <*rr*> . n >= 0 ) ) ) by ; :: thesis: verum
end;
u in { w where w is Element of V : L . w <> 0 } by A18;
then A22: u in Carrier L by RLVECT_2:def 4;
v in { w where w is Element of V : L . w <> 0 } by ;
then v in Carrier L by RLVECT_2:def 4;
then ( Carrier L c= {u,v} & {u,v} c= Carrier L ) by ;
then Carrier L = {u,v} by XBOOLE_0:def 10;
then Carrier L = {u} by ;
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 ; :: thesis: verum
end;
then L is convex ;
then A23: Sum L in M by A1, A5;
(r * u) + ((1 - r) * v) = (r + (1 - r)) * u by
.= (0 + 1) * u ;
hence (rr * u) + ((1 - rr) * v) in M by ; :: thesis: verum
end;
end;
end;
hence (rr * u) + ((1 - rr) * v) in M ; :: thesis: verum