let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r, s being Real st s > 0 holds
( (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) = Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) )
let p be Point of (TOP-REAL n); :: thesis: for r, s being Real st s > 0 holds
( (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) = Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) )
let r, s be Real; :: thesis: ( s > 0 implies ( (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) = Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) ) )
assume A1: s > 0 ; :: thesis: ( (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) = Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) )
set TR = TOP-REAL n;
set M = mlt (s,(TOP-REAL n));
set ss = |.s.|;
set s1 = 1 / s;
A2: |.s.| = s by A1, ABSVALUE:def 1;
A4: dom (mlt (s,(TOP-REAL n))) = [#] (TOP-REAL n) by FUNCT_2:def 1;
A5: s * (1 / s) = 1 by A1, XCMPLX_1:87;
thus (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) = Ball ((s * p),(r * s)) :: thesis: ( (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) )

proof

thus (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) c= Ball ((s * p),(r * s)) :: according to XBOOLE_0:def 10 :: thesis: Ball ((s * p),(r * s)) c= (mlt (s,(TOP-REAL n))) .: (Ball (p,r))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) or y in Ball ((s * p),(r * s)) )
assume y in (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) ; :: thesis: y in Ball ((s * p),(r * s))
then consider x being object such that
A6: x in dom (mlt (s,(TOP-REAL n))) and
A7: x in Ball (p,r) and
A8: (mlt (s,(TOP-REAL n))) . x = y by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL n) by A6;
A9: y = s * q by A8, RLTOPSP1:def 13;
(s * q) - (s * p) = s * (q - p) by RLVECT_1:34;
then A10: |.((s * q) - (s * p)).| = s * |.(q - p).| by A2, EUCLID:11;
s * |.(q - p).| < r * s by A7, TOPREAL9:7, A1, XREAL_1:68;
hence y in Ball ((s * p),(r * s)) by A10, A9; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball ((s * p),(r * s)) or y in (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) )
A11: (r * s) * (1 / s) = r * (s * (1 / s)) ;
assume A12: y in Ball ((s * p),(r * s)) ; :: thesis: y in (mlt (s,(TOP-REAL n))) .: (Ball (p,r))
then reconsider q = y as Point of (TOP-REAL n) ;
A13: (|.(((1 / s) * q) - p).| * s) * (1 / s) = |.(((1 / s) * q) - p).| * (s * (1 / s)) ;
A14: s * ((1 / s) * q) = (s * (1 / s)) * q by RLVECT_1:def 7
.= 1 * q by A1, XCMPLX_1:87
.= q by RLVECT_1:def 8 ;
then |.(q - (s * p)).| = |.(s * (((1 / s) * q) - p)).| by RLVECT_1:34
.= s * |.(((1 / s) * q) - p).| by A2, EUCLID:11 ;
then |.(((1 / s) * q) - p).| < r by A11, A13, A5, A12, TOPREAL9:7, A1, XREAL_1:68;
then A15: (1 / s) * q in Ball (p,r) ;
(mlt (s,(TOP-REAL n))) . ((1 / s) * q) = q by A14, RLTOPSP1:def 13;
hence y in (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) by A4, A15, FUNCT_1:def 6; :: thesis: verum

end;

thus (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) :: thesis: (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s))

proof

thus (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) c= cl_Ball ((s * p),(r * s)) :: according to XBOOLE_0:def 10 :: thesis: cl_Ball ((s * p),(r * s)) c= (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) or y in cl_Ball ((s * p),(r * s)) )
assume y in (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) ; :: thesis: y in cl_Ball ((s * p),(r * s))
then consider x being object such that
A16: x in dom (mlt (s,(TOP-REAL n))) and
A17: x in cl_Ball (p,r) and
A18: (mlt (s,(TOP-REAL n))) . x = y by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL n) by A16;
A19: y = s * q by A18, RLTOPSP1:def 13;
(s * q) - (s * p) = s * (q - p) by RLVECT_1:34;
then A20: |.((s * q) - (s * p)).| = s * |.(q - p).| by A2, EUCLID:11;
s * |.(q - p).| <= r * s by A17, TOPREAL9:8, A1, XREAL_1:64;
hence y in cl_Ball ((s * p),(r * s)) by A20, A19; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in cl_Ball ((s * p),(r * s)) or y in (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) )
A21: (r * s) * (1 / s) = r * (s * (1 / s)) ;
assume A22: y in cl_Ball ((s * p),(r * s)) ; :: thesis: y in (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r))
then reconsider q = y as Point of (TOP-REAL n) ;
A23: (|.(((1 / s) * q) - p).| * s) * (1 / s) = |.(((1 / s) * q) - p).| * (s * (1 / s)) ;
A24: s * ((1 / s) * q) = (s * (1 / s)) * q by RLVECT_1:def 7
.= 1 * q by A1, XCMPLX_1:87
.= q by RLVECT_1:def 8 ;
then |.(q - (s * p)).| = |.(s * (((1 / s) * q) - p)).| by RLVECT_1:34
.= s * |.(((1 / s) * q) - p).| by A2, EUCLID:11 ;
then |.(((1 / s) * q) - p).| <= r by A21, A23, A5, A22, TOPREAL9:8, A1, XREAL_1:64;
then A25: (1 / s) * q in cl_Ball (p,r) ;
(mlt (s,(TOP-REAL n))) . ((1 / s) * q) = q by A24, RLTOPSP1:def 13;
hence y in (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) by A4, A25, FUNCT_1:def 6; :: thesis: verum

end;

thus (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) c= Sphere ((s * p),(r * s)) :: according to XBOOLE_0:def 10 :: thesis: Sphere ((s * p),(r * s)) c= (mlt (s,(TOP-REAL n))) .: (Sphere (p,r))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) or y in Sphere ((s * p),(r * s)) )
assume y in (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) ; :: thesis: y in Sphere ((s * p),(r * s))
then consider x being object such that
A26: x in dom (mlt (s,(TOP-REAL n))) and
A27: x in Sphere (p,r) and
A28: (mlt (s,(TOP-REAL n))) . x = y by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL n) by A26;
(s * q) - (s * p) = s * (q - p) by RLVECT_1:34;
then A29: |.((s * q) - (s * p)).| = s * |.(q - p).| by A2, EUCLID:11;
s * |.(q - p).| = r * s by A27, TOPREAL9:9;
then s * q in Sphere ((s * p),(r * s)) by A29;
hence y in Sphere ((s * p),(r * s)) by A28, RLTOPSP1:def 13; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Sphere ((s * p),(r * s)) or y in (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) )
assume A30: y in Sphere ((s * p),(r * s)) ; :: thesis: y in (mlt (s,(TOP-REAL n))) .: (Sphere (p,r))
then reconsider q = y as Point of (TOP-REAL n) ;
A31: (|.(((1 / s) * q) - p).| * s) * (1 / s) = |.(((1 / s) * q) - p).| * (s * (1 / s)) ;
A32: (r * s) * (1 / s) = r * (s * (1 / s)) ;
A33: s * ((1 / s) * q) = (s * (1 / s)) * q by RLVECT_1:def 7
.= 1 * q by A1, XCMPLX_1:87
.= q by RLVECT_1:def 8 ;
then |.(q - (s * p)).| = |.(s * (((1 / s) * q) - p)).| by RLVECT_1:34
.= s * |.(((1 / s) * q) - p).| by A2, EUCLID:11 ;
then |.(((1 / s) * q) - p).| = r by A32, A31, A5, A30, TOPREAL9:9;
then A34: (1 / s) * q in Sphere (p,r) ;
(mlt (s,(TOP-REAL n))) . ((1 / s) * q) = q by A33, RLTOPSP1:def 13;
hence y in (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) by A4, A34, FUNCT_1:def 6; :: thesis: verum