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 )
set S = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ;
assume A1: M is convex ; :: thesis: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= M
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } or 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 and
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 A3: card (Carrier L) < 2 ; :: thesis: v in M

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

end;

suppose A7: 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;
A8: 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
A9: card (Carrier LL) = 1 + 1 and
A10: 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
A11: ( 0 < r & r < 1 ) and
A12: LL = (r * L1) + ((1 - r) * L2) and
A13: card (Carrier L1) = 1 and
A14: card (Carrier L2) = (card (Carrier LL)) - 1 by A10;
consider x2 being object such that
A15: Carrier L2 = {x2} by A9, A14, CARD_2:42;
x2 in Carrier L2 by A15, TARSKI:def 1;
then reconsider x2 = x2 as VECTOR of V ;
( Sum L2 = (L2 . x2) * x2 & L2 . x2 = 1 ) by A15, CONVEX1:27, RLVECT_2:35;
then A16: Sum L2 = x2 by RLVECT_1:def 8;
{x2} c= M by A15, RLVECT_2:def 6;
then A17: Sum L2 in M by A16, ZFMISC_1:31;
consider x1 being object such that
A18: Carrier L1 = {x1} by A13, CARD_2:42;
x1 in Carrier L1 by A18, TARSKI:def 1;
then reconsider x1 = x1 as VECTOR of V ;
( Sum L1 = (L1 . x1) * x1 & L1 . x1 = 1 ) by A18, CONVEX1:27, RLVECT_2:35;
then A19: Sum L1 = x1 by RLVECT_1:def 8;
{x1} c= M by A18, RLVECT_2:def 6;
then A20: Sum L1 in M by A19, ZFMISC_1:31;
Sum LL = (Sum (r * L1)) + (Sum ((1 - r) * L2)) by A12, 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, A11, A20, A17, CONVEX1:def 2; :: thesis: verum

end;

consider k being Nat such that
A21: card (Carrier L) = k + 1 by A7, NAT_1:6;
reconsider k = k as non zero Element of NAT by A7, A21, ORDINAL1:def 12;
A22: card (Carrier L) = 1 + k by A21;
A23: 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 A7, Lm2;
A24: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A25: 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
A26: card (Carrier LL) = 1 + (k + 1) and
A27: 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
A28: ( 0 < r & r < 1 ) and
A29: LL = (r * L1) + ((1 - r) * L2) and
A30: card (Carrier L1) = 1 and
A31: card (Carrier L2) = (card (Carrier LL)) - 1 by A27;
k >= 0 + 1 by NAT_1:13;
then k + 1 >= 1 + 1 by XREAL_1:6;
then ex LL1, LL2 being Convex_Combination of M ex rr being Real st
( 0 < rr & rr < 1 & L2 = (rr * LL1) + ((1 - rr) * LL2) & card (Carrier LL1) = 1 & card (Carrier LL2) = (card (Carrier L2)) - 1 ) by A26, A31, Lm2;
then A32: Sum L2 in M by A25, A26, A31;
consider x1 being object such that
A33: Carrier L1 = {x1} by A30, CARD_2:42;
x1 in Carrier L1 by A33, TARSKI:def 1;
then reconsider x1 = x1 as VECTOR of V ;
( Sum L1 = (L1 . x1) * x1 & L1 . x1 = 1 ) by A33, CONVEX1:27, RLVECT_2:35;
then A34: Sum L1 = x1 by RLVECT_1:def 8;
{x1} c= M by A33, RLVECT_2:def 6;
then A35: Sum L1 in M by A34, ZFMISC_1:31;
Sum LL = (Sum (r * L1)) + (Sum ((1 - r) * L2)) by A29, 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, A28, A35, A32, CONVEX1:def 2; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A8, A24);
hence v in M by A2, A22, A23; :: thesis: verum

end;

end;