let V be RealLinearSpace; :: thesis: for M being non empty Subset of V holds conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V }
let M be non empty Subset of V; :: thesis: conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V }
consider m being object such that
A1: m in M by XBOOLE_0:def 1;
reconsider m = m as VECTOR of V by A1;
consider LL being Convex_Combination of V such that
A2: Sum LL = m and
A3: for A being non empty Subset of V st m in A holds
LL is Convex_Combination of A by Th1;
reconsider LL = LL as Convex_Combination of M by A1, A3;
LL in ConvexComb V by Def1;
then m in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A2;
then reconsider N = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } as non empty set ;
for x being object st x in N holds
x in the carrier of V

proof

let x be object ; :: thesis: ( x in N implies x in the carrier of V )
assume x in N ; :: thesis: x in the carrier of V
then ex L being Convex_Combination of M st
( x = Sum L & L in ConvexComb V ) ;
hence x in the carrier of V ; :: thesis: verum

end;

then reconsider N = N as Subset of V by TARSKI:def 3;
for x being object st x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } holds
x in conv M

proof

let x be object ; :: thesis: ( x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } implies x in conv M )
assume x in { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } ; :: thesis: x in conv M
then A4: ex L being Convex_Combination of M st
( x = Sum L & L in ConvexComb V ) ;
M c= conv M by CONVEX1:41;
hence x in conv M by A4, CONVEX2:6; :: thesis: verum

end;

then A5: { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } c= conv M ;
for u, v being VECTOR of V
for r being Real st 0 < r & r < 1 & u in N & v in N holds
(r * u) + ((1 - r) * v) in N

proof

let u, v be VECTOR of V; :: thesis: for r being Real st 0 < r & r < 1 & u in N & v in N holds
(r * u) + ((1 - r) * v) in N
let r be Real; :: thesis: ( 0 < r & r < 1 & u in N & v in N implies (r * u) + ((1 - r) * v) in N )
assume that
A6: ( 0 < r & r < 1 ) and
A7: u in N and
A8: v in N ; :: thesis: (r * u) + ((1 - r) * v) in N
consider Lv being Convex_Combination of M such that
A9: v = Sum Lv and
Lv in ConvexComb V by A8;
consider Lu being Convex_Combination of M such that
A10: u = Sum Lu and
Lu in ConvexComb V by A7;
reconsider r = r as Real ;
reconsider LL = (r * Lu) + ((1 - r) * Lv) as Convex_Combination of M by A6, CONVEX2:9;
(r * Lu) + ((1 - r) * Lv) is Convex_Combination of V by A6, CONVEX2:8;
then A11: (r * Lu) + ((1 - r) * Lv) in ConvexComb V by Def1;
Sum LL = (Sum (r * Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:1
.= (r * (Sum Lu)) + (Sum ((1 - r) * Lv)) by RLVECT_3:2
.= (r * (Sum Lu)) + ((1 - r) * (Sum Lv)) by RLVECT_3:2 ;
hence (r * u) + ((1 - r) * v) in N by A10, A9, A11; :: thesis: verum

end;

then A12: N is convex by CONVEX1:def 2;
for v being object st v in M holds
v in N

proof

let v be object ; :: thesis: ( v in M implies v in N )
assume A13: v in M ; :: thesis: v in N
then reconsider v = v as VECTOR of V ;
consider LL being Convex_Combination of V such that
A14: Sum LL = v and
A15: for A being non empty Subset of V st v in A holds
LL is Convex_Combination of A by Th1;
reconsider LL = LL as Convex_Combination of M by A13, A15;
LL in ConvexComb V by Def1;
hence v in N by A14; :: thesis: verum

end;

then M c= N ;
then conv M c= N by A12, CONVEX1:30;
hence conv M = { (Sum L) where L is Convex_Combination of M : L in ConvexComb V } by A5, XBOOLE_0:def 10; :: thesis: verum