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 object ; :: 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 r * M = {(0. V)} by A1, CONVEX1:34;
then A3: {(0. V)} c= Cir (r * M) by Th11;
Cir M <> {} by A2, Th11, XBOOLE_1:3;
then r * (Cir M) = {(0. V)} by A1, CONVEX1:34;
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 A8: W in Circled-Family (r * M) ; :: thesis: r * v in W
then reconsider W = W as Subset of V ;
r * M c= W by A8, 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 A9: M c= (r ") * W by CONVEX1:32;
W is circled by A8, Def2;
then (r ") * W is circled by Th2;
then (r ") * W in Circled-Family M by A9, Def2;
then ( (r ") * W = { ((r ") * w) where w is Point of V : w in W } & v in (r ") * W ) by A7, CONVEX1:def 1, SETFAM_1:def 1;
then consider w being Point of V such that
A10: v = (r ") * w and
A11: w in W ;
r * v = (r * (r ")) * w by A10, RLVECT_1:def 7
.= 1 * w by A4, XCMPLX_0:def 7
.= w by RLVECT_1:def 8 ;
hence r * v in W by A11; :: thesis: verum

end;

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

end;

end;

end;

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