let X be RealLinearSpace; :: thesis: for M being Subset of X
for r being Real holds r * (conv M) = conv (r * M)
let M be Subset of X; :: thesis: for r being Real holds r * (conv M) = conv (r * M)
let r be Real; :: thesis: r * (conv M) = conv (r * M)
thus r * (conv M) c= conv (r * M) :: according to XBOOLE_0:def 10 :: thesis: conv (r * M) c= r * (conv M)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

per cases ( r = 0 or r <> 0 ) ;

suppose A1: r = 0 ; :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

per cases ( M = {} or M <> {} ) ;

suppose M = {} ; :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

hence ( not x in r * (conv M) or x in conv (r * M) ) by CONVEX1:33; :: thesis: verum

end;

suppose A2: M <> {} ; :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

then r * M = {(0. X)} by A1, CONVEX1:34;
then A3: {(0. X)} c= conv (r * M) by CONVEX1:41;
conv M <> {} by A2, CONVEX1:41, XBOOLE_1:3;
then r * (conv M) = {(0. X)} by A1, CONVEX1:34;
hence ( not x in r * (conv M) or x in conv (r * M) ) by A3; :: thesis: verum

end;

end;

end;

suppose A4: r <> 0 ; :: thesis: ( not x in r * (conv M) or x in conv (r * M) )

assume x in r * (conv M) ; :: thesis: x in conv (r * M)
then consider v being Point of X such that
A5: x = r * v and
A6: v in conv M ;
for V being set st V in Convex-Family (r * M) holds
r * v in V

proof

let V be set ; :: thesis: ( V in Convex-Family (r * M) implies r * v in V )
assume A7: V in Convex-Family (r * M) ; :: thesis: r * v in V
then reconsider V = V as Subset of X ;
r * M c= V by A7, CONVEX1:def 4;
then (r ") * (r * M) c= (r ") * V by CONVEX1:39;
then ((r ") * r) * M c= (r ") * V by CONVEX1:37;
then 1 * M c= (r ") * V by A4, XCMPLX_0:def 7;
then A8: M c= (r ") * V by CONVEX1:32;
V is convex by A7, CONVEX1:def 4;
then (r ") * V is convex by CONVEX1:1;
then (r ") * V in Convex-Family M by A8, CONVEX1:def 4;
then v in (r ") * V by A6, SETFAM_1:def 1;
then consider w being Point of X such that
A9: v = (r ") * w and
A10: w in V ;
r * v = (r * (r ")) * w by A9, RLVECT_1:def 7
.= 1 * w by A4, XCMPLX_0:def 7
.= w by RLVECT_1:def 8 ;
hence r * v in V by A10; :: thesis: verum

end;

hence x in conv (r * M) by A5, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

( r * M c= r * (conv M) & r * (conv M) is convex ) by CONVEX1:1, CONVEX1:39, CONVEX1:41;
hence conv (r * M) c= r * (conv M) by CONVEX1:30; :: thesis: verum