let V be RealLinearSpace; :: thesis: for M being non empty Subset of V st M is convex holds
{ (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M
let M be non empty Subset of V; :: thesis: ( M is convex implies { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M )
assume A1: M is convex ; :: thesis: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M
set S = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ;
for v being set st v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } holds
v in M

proof

let v be set ; :: thesis: ( v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } implies v in M )
assume v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ; :: thesis: v in M
then consider L being Convex_Combination of M such that
A2: ( v = Sum L & L in ConvexComb V ) ;
reconsider v = v as VECTOR of V by A2;

per cases ( card (Carrier L) < 2 or card (Carrier L) >= 2 ) ;

suppose card (Carrier L) < 2 ; :: thesis: v in M

then card (Carrier L) < 1 + 1 ;
then A3: card (Carrier L) <= 1 by NAT_1:13;
Carrier L <> 0 by CONVEX1:21;
then card (Carrier L) > 0 ;
then card (Carrier L) >= 0 + 1 by NAT_1:13;
then card (Carrier L) = 1 by A3, XXREAL_0:1;
then consider x being set such that
A4: Carrier L = {x} by CARD_2:60;
x in Carrier L by A4, TARSKI:def 1;
then reconsider x = x as VECTOR of V ;
A5: v = (L . x) * x by A2, A4, RLVECT_2:53
.= 1 * x by A4, CONVEX1:27
.= x by RLVECT_1:def 9 ;
{x} c= M by A4, RLVECT_2:def 8;
hence v in M by A5, ZFMISC_1:37; :: thesis: verum

end;

suppose A6: card (Carrier L) >= 2 ; :: thesis: v in M

defpred S₁[ Nat] means for LL being Convex_Combination of M st card (Carrier LL) = 1 + $1 & ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) holds
Sum LL in M;
A7: S₁[1]

proof

let LL be Convex_Combination of M; :: thesis: ( card (Carrier LL) = 1 + 1 & ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) implies Sum LL in M )
assume that
A8: card (Carrier LL) = 1 + 1 and
A9: ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) ; :: thesis: Sum LL in M
consider L1, L2 being Convex_Combination of M, r being Real such that
A10: ( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) by A9;
consider x1 being set such that
A11: Carrier L1 = {x1} by A10, CARD_2:60;
x1 in Carrier L1 by A11, TARSKI:def 1;
then reconsider x1 = x1 as VECTOR of V ;
( Sum L1 = (L1 . x1) * x1 & L1 . x1 = 1 ) by A11, CONVEX1:27, RLVECT_2:53;
then A12: Sum L1 = x1 by RLVECT_1:def 9;
A13: {x1} c= M by A11, RLVECT_2:def 8;
consider x2 being set such that
A14: Carrier L2 = {x2} by A8, A10, CARD_2:60;
x2 in Carrier L2 by A14, TARSKI:def 1;
then reconsider x2 = x2 as VECTOR of V ;
( Sum L2 = (L2 . x2) * x2 & L2 . x2 = 1 ) by A14, CONVEX1:27, RLVECT_2:53;
then A15: Sum L2 = x2 by RLVECT_1:def 9;
{x2} c= M by A14, RLVECT_2:def 8;
then A16: ( Sum L1 in M & Sum L2 in M ) by A12, A13, A15, ZFMISC_1:37;
Sum LL = (Sum (r * L1)) + (Sum ((1 - r) * L2)) by A10, RLVECT_3:1
.= (r * (Sum L1)) + (Sum ((1 - r) * L2)) by RLVECT_3:2
.= (r * (Sum L1)) + ((1 - r) * (Sum L2)) by RLVECT_3:2 ;
hence Sum LL in M by A1, A10, A16, CONVEX1:def 2; :: thesis: verum

end;

A17: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non empty Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A18: S₁[k] ; :: thesis: S₁[k + 1]
let LL be Convex_Combination of M; :: thesis: ( card (Carrier LL) = 1 + (k + 1) & ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) implies Sum LL in M )
assume that
A19: card (Carrier LL) = 1 + (k + 1) and
A20: ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) ; :: thesis: Sum LL in M
consider L1, L2 being Convex_Combination of M, r being Real such that
A21: ( 0 < r & r < 1 & LL = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier LL)) - 1 ) by A20;
consider x1 being set such that
A22: Carrier L1 = {x1} by A21, CARD_2:60;
x1 in Carrier L1 by A22, TARSKI:def 1;
then reconsider x1 = x1 as VECTOR of V ;
( Sum L1 = (L1 . x1) * x1 & L1 . x1 = 1 ) by A22, CONVEX1:27, RLVECT_2:53;
then A23: Sum L1 = x1 by RLVECT_1:def 9;
{x1} c= M by A22, RLVECT_2:def 8;
then A24: Sum L1 in M by A23, ZFMISC_1:37;
k >= 0 + 1 by NAT_1:13;
then k + 1 >= 1 + 1 by XREAL_1:8;
then consider LL1, LL2 being Convex_Combination of M, rr being Real such that
A25: ( 0 < rr & rr < 1 & L2 = (rr * LL1) + ((1 - rr) * LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L2)) - 1 ) by A19, A21, Lm2;
A26: Sum L2 in M by A18, A19, A21, A25;
Sum LL = (Sum (r * L1)) + (Sum ((1 - r) * L2)) by A21, RLVECT_3:1
.= (r * (Sum L1)) + (Sum ((1 - r) * L2)) by RLVECT_3:2
.= (r * (Sum L1)) + ((1 - r) * (Sum L2)) by RLVECT_3:2 ;
hence Sum LL in M by A1, A21, A24, A26, CONVEX1:def 2; :: thesis: verum

end;

A27: for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A7, A17);
consider k being Nat such that
A28: card (Carrier L) = k + 1 by A6, NAT_1:6;
reconsider k = k as non empty Element of NAT by A6, A28, ORDINAL1:def 13;
A29: card (Carrier L) = 1 + k by A28;
ex L1, L2 being Convex_Combination of M ex r being Real st
( 0 < r & r < 1 & L = (r * L1) + ((1 - r) * L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 ) by A6, Lm2;
hence v in M by A2, A27, A29; :: thesis: verum

end;

end;

end;

hence { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M by TARSKI:def 3; :: thesis: verum