let n be Nat; :: thesis: for r, s being Real st r > 0 holds
for x being Element of (Euclid n) st x = 0* n holds
for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds
r * A = Ball (x,(r * s))
let r, s be Real; :: thesis: ( r > 0 implies for x being Element of (Euclid n) st x = 0* n holds
for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds
r * A = Ball (x,(r * s)) )
assume A1: r > 0 ; :: thesis: for x being Element of (Euclid n) st x = 0* n holds
for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds
r * A = Ball (x,(r * s))
let x be Element of (Euclid n); :: thesis: ( x = 0* n implies for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds
r * A = Ball (x,(r * s)) )
assume A2: x = 0* n ; :: thesis: for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds
r * A = Ball (x,(r * s))
let A be Subset of (TOP-REAL n); :: thesis: ( A = Ball (x,s) implies r * A = Ball (x,(r * s)) )
assume A3: A = Ball (x,s) ; :: thesis: r * A = Ball (x,(r * s))
thus r * A c= Ball (x,(r * s)) :: according to XBOOLE_0:def 10 :: thesis: Ball (x,(r * s)) c= r * A

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in r * A or y in Ball (x,(r * s)) )
assume y in r * A ; :: thesis: y in Ball (x,(r * s))
then consider v being Element of (TOP-REAL n) such that
A4: y = r * v and
A5: v in A ;
v in { q where q is Element of (Euclid n) : dist (x,q) < s } by A5, A3, METRIC_1:def 14;
then consider q being Element of (Euclid n) such that
A6: v = q and
A7: dist (x,q) < s ;
reconsider p = y as Element of (Euclid n) by A4, EUCLID:67;
r * (dist (x,q)) = dist (x,p) by A1, A2, A6, A4, Lm1;
then dist (x,p) < r * s by A7, A1, XREAL_1:68;
then y in { e where e is Element of (Euclid n) : dist (x,e) < r * s } ;
hence y in Ball (x,(r * s)) by METRIC_1:def 14; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (x,(r * s)) or y in r * A )
assume y in Ball (x,(r * s)) ; :: thesis: y in r * A
then y in { q where q is Element of (Euclid n) : dist (x,q) < r * s } by METRIC_1:def 14;
then consider z being Element of (Euclid n) such that
A8: y = z and
A9: dist (x,z) < r * s ;
reconsider q = z as Element of (TOP-REAL n) by EUCLID:67;
set p = (r ") * q;
A10: y = 1 * q by A8, RVSUM_1:52
.= ((r ") * r) * q by A1, XCMPLX_0:def 7
.= r * ((r ") * q) by RVSUM_1:49 ;
reconsider f = (r ") * q as Element of (Euclid n) by EUCLID:67;
A11: dist (x,f) = (r ") * (dist (x,z)) by A1, A2, Lm1;
s = 1 * s
.= ((r ") * ((r ") ")) * s by A1, XCMPLX_0:def 7
.= (r ") * (r * s) ;
then dist (x,f) < s by A9, A11, A1, XREAL_1:68;
then (r ") * q in { e where e is Element of (Euclid n) : dist (x,e) < s } ;
then (r ") * q in A by A3, METRIC_1:def 14;
hence y in r * A by A10; :: thesis: verum