let X be LinearTopSpace; :: thesis: for A being Subset of X
for r being non zero Real holds r * (Cl A) = Cl (r * A)
let A be Subset of X; :: thesis: for r being non zero Real holds r * (Cl A) = Cl (r * A)
let r be non zero Real; :: thesis: r * (Cl A) = Cl (r * A)
thus r * (Cl A) c= Cl (r * A) :: according to XBOOLE_0:def 10 :: thesis: Cl (r * A) c= r * (Cl A)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in r * (Cl A) or z in Cl (r * A) )
assume A1: z in r * (Cl A) ; :: thesis: z in Cl (r * A)
then reconsider z = z as Point of X ;

now :: thesis: for G being Subset of X st G is open & z in G holds
r * A meets G

let G be Subset of X; :: thesis: ( G is open & z in G implies r * A meets G )
assume ( G is open & z in G ) ; :: thesis: r * A meets G
then A2: ( (r ") * z in (r ") * G & (r ") * G is open ) by Th49;
consider v being Point of X such that
A3: z = r * v and
A4: v in Cl A by A1;
(r ") * z = ((r ") * r) * v by A3, RLVECT_1:def 7
.= 1 * v by XCMPLX_0:def 7
.= v by RLVECT_1:def 8 ;
then A meets (r ") * G by A4, A2, PRE_TOPC:24;
then consider x being object such that
A5: x in A and
A6: x in (r ") * G by XBOOLE_0:3;
reconsider x = x as Point of X by A5;
consider u being Point of X such that
A7: x = (r ") * u and
A8: u in G by A6;
A9: r * x in r * A by A5;
r * x = (r * (r ")) * u by A7, RLVECT_1:def 7
.= 1 * u by XCMPLX_0:def 7
.= u by RLVECT_1:def 8 ;
hence r * A meets G by A8, A9, XBOOLE_0:3; :: thesis: verum

end;

hence z in Cl (r * A) by PRE_TOPC:24; :: thesis: verum

end;

r * A c= r * (Cl A) by CONVEX1:39, PRE_TOPC:18;
hence Cl (r * A) c= r * (Cl A) by Th50, TOPS_1:5; :: thesis: verum