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

proof

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

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

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

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

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

then M = {} V ;
then Cir M = {} by Th14;
hence ( not x in r * (Cir M) or x in Cir (r * M) ) by CONVEX1:33; :: thesis: verum

end;

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

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

end;

end;

end;

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

A5: r * (Cir M) = { (r * v) where v is Point of V : v in Cir M } by CONVEX1:def 1;
assume x in r * (Cir M) ; :: thesis: x in Cir (r * M)
then consider v being Point of V such that
A6: x = r * v and
A7: v in Cir M by A5;
for W being set st W in Circled-Family (r * M) holds
r * v in W

proof

let W be set ; :: thesis: ( W in Circled-Family (r * M) implies r * v in W )
assume A9: W in Circled-Family (r * M) ; :: thesis: r * v in W
then reconsider W = W as Subset of V ;
A10: W is circled by A9, Def2;
r * M c= W by A9, Def2;
then (r " ) * (r * M) c= (r " ) * W by CONVEX1:39;
then ((r " ) * r) * M c= (r " ) * W by CONVEX1:37;
then 1 * M c= (r " ) * W by A4, XCMPLX_0:def 7;
then A11: M c= (r " ) * W by CONVEX1:32;
A12: (r " ) * W = { ((r " ) * w) where w is Point of V : w in W } by CONVEX1:def 1;
(r " ) * W is circled by A10, Th2;
then (r " ) * W in Circled-Family M by A11, Def2;
then v in (r " ) * W by A7, SETFAM_1:def 1;
then consider w being Point of V such that
A13: v = (r " ) * w and
A14: w in W by A12;
r * v = (r * (r " )) * w by A13, RLVECT_1:def 9
.= 1 * w by A4, XCMPLX_0:def 7
.= w by RLVECT_1:def 9 ;
hence r * v in W by A14; :: thesis: verum

end;

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

end;

end;

end;

A15: r * M c= r * (Cir M) by Th11, CONVEX1:39;
r * (Cir M) is circled by Th2;
hence Cir (r * M) c= r * (Cir M) by A15, Th12; :: thesis: verum