let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)

for r, s being positive Real holds Tball (p,r), Tball (q,s) are_homeomorphic

let p, q be Point of (TOP-REAL n); :: thesis: for r, s being positive Real holds Tball (p,r), Tball (q,s) are_homeomorphic

set TR = TOP-REAL n;

let r, s be positive Real; :: thesis: Tball (p,r), Tball (q,s) are_homeomorphic

Ball (q,s) c= Int (cl_Ball (q,s)) by TOPREAL9:16, TOPS_1:24;

then A2: ( not cl_Ball (q,s) is boundary & cl_Ball (q,s) is compact ) ;

Ball (p,r) c= Int (cl_Ball (p,r)) by TOPREAL9:16, TOPS_1:24;

then ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact ) ;

then consider h being Function of ((TOP-REAL n) | (cl_Ball (p,r))),((TOP-REAL n) | (cl_Ball (q,s))) such that

A4: ( h is being_homeomorphism & h .: (Fr (cl_Ball (p,r))) = Fr (cl_Ball (q,s)) ) by A2, BROUWER2:7;

A5: [#] ((TOP-REAL n) | (cl_Ball (q,s))) = cl_Ball (q,s) by PRE_TOPC:def 5;

A6: h .: (dom h) = rng h by RELAT_1:113

.= [#] ((TOP-REAL n) | (cl_Ball (q,s))) by FUNCT_2:def 3, A4 ;

A7: Fr (cl_Ball (p,r)) = Sphere (p,r) by BROUWER2:5;

A8: [#] ((TOP-REAL n) | (cl_Ball (p,r))) = cl_Ball (p,r) by PRE_TOPC:def 5;

A9: ( (Ball (q,s)) \/ (Sphere (q,s)) = cl_Ball (q,s) & Ball (q,s) misses Sphere (q,s) ) by TOPREAL9:18, TOPREAL9:19;

A10: ( (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) & Ball (p,r) misses Sphere (p,r) ) by TOPREAL9:18, TOPREAL9:19;

reconsider Br = Ball (p,r) as Subset of ((TOP-REAL n) | (cl_Ball (p,r))) by A10, A8, XBOOLE_1:7;

reconsider Bs = Ball (q,s) as Subset of ((TOP-REAL n) | (cl_Ball (q,s))) by A9, A5, XBOOLE_1:7;

A12: dom h = [#] ((TOP-REAL n) | (cl_Ball (p,r))) by FUNCT_2:def 1;

A13: ( (Ball (q,s)) \/ (Sphere (q,s)) = cl_Ball (q,s) & Ball (q,s) misses Sphere (q,s) ) by TOPREAL9:18, TOPREAL9:19;

A14: ( (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) & Ball (p,r) misses Sphere (p,r) ) by TOPREAL9:18, TOPREAL9:19;

(dom h) \ (Sphere (p,r)) = Ball (p,r) by A12, A8, XBOOLE_1:88, A14;

then h .: Br = (h .: (dom h)) \ (Fr (cl_Ball (q,s))) by A4, FUNCT_1:64, A7

.= (cl_Ball (q,s)) \ (Sphere (q,s)) by BROUWER2:5, A6, A5

.= Bs by A13, XBOOLE_1:88 ;

then ((TOP-REAL n) | (cl_Ball (p,r))) | Br,((TOP-REAL n) | (cl_Ball (q,s))) | Bs are_homeomorphic by A4, METRIZTS:3, METRIZTS:def 1;

then (TOP-REAL n) | (Ball (p,r)),((TOP-REAL n) | (cl_Ball (q,s))) | Bs are_homeomorphic by PRE_TOPC:7, A8;

hence Tball (p,r), Tball (q,s) are_homeomorphic by PRE_TOPC:7, A5; :: thesis: verum

for r, s being positive Real holds Tball (p,r), Tball (q,s) are_homeomorphic

let p, q be Point of (TOP-REAL n); :: thesis: for r, s being positive Real holds Tball (p,r), Tball (q,s) are_homeomorphic

set TR = TOP-REAL n;

let r, s be positive Real; :: thesis: Tball (p,r), Tball (q,s) are_homeomorphic

Ball (q,s) c= Int (cl_Ball (q,s)) by TOPREAL9:16, TOPS_1:24;

then A2: ( not cl_Ball (q,s) is boundary & cl_Ball (q,s) is compact ) ;

Ball (p,r) c= Int (cl_Ball (p,r)) by TOPREAL9:16, TOPS_1:24;

then ( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact ) ;

then consider h being Function of ((TOP-REAL n) | (cl_Ball (p,r))),((TOP-REAL n) | (cl_Ball (q,s))) such that

A4: ( h is being_homeomorphism & h .: (Fr (cl_Ball (p,r))) = Fr (cl_Ball (q,s)) ) by A2, BROUWER2:7;

A5: [#] ((TOP-REAL n) | (cl_Ball (q,s))) = cl_Ball (q,s) by PRE_TOPC:def 5;

A6: h .: (dom h) = rng h by RELAT_1:113

.= [#] ((TOP-REAL n) | (cl_Ball (q,s))) by FUNCT_2:def 3, A4 ;

A7: Fr (cl_Ball (p,r)) = Sphere (p,r) by BROUWER2:5;

A8: [#] ((TOP-REAL n) | (cl_Ball (p,r))) = cl_Ball (p,r) by PRE_TOPC:def 5;

A9: ( (Ball (q,s)) \/ (Sphere (q,s)) = cl_Ball (q,s) & Ball (q,s) misses Sphere (q,s) ) by TOPREAL9:18, TOPREAL9:19;

A10: ( (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) & Ball (p,r) misses Sphere (p,r) ) by TOPREAL9:18, TOPREAL9:19;

reconsider Br = Ball (p,r) as Subset of ((TOP-REAL n) | (cl_Ball (p,r))) by A10, A8, XBOOLE_1:7;

reconsider Bs = Ball (q,s) as Subset of ((TOP-REAL n) | (cl_Ball (q,s))) by A9, A5, XBOOLE_1:7;

A12: dom h = [#] ((TOP-REAL n) | (cl_Ball (p,r))) by FUNCT_2:def 1;

A13: ( (Ball (q,s)) \/ (Sphere (q,s)) = cl_Ball (q,s) & Ball (q,s) misses Sphere (q,s) ) by TOPREAL9:18, TOPREAL9:19;

A14: ( (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) & Ball (p,r) misses Sphere (p,r) ) by TOPREAL9:18, TOPREAL9:19;

(dom h) \ (Sphere (p,r)) = Ball (p,r) by A12, A8, XBOOLE_1:88, A14;

then h .: Br = (h .: (dom h)) \ (Fr (cl_Ball (q,s))) by A4, FUNCT_1:64, A7

.= (cl_Ball (q,s)) \ (Sphere (q,s)) by BROUWER2:5, A6, A5

.= Bs by A13, XBOOLE_1:88 ;

then ((TOP-REAL n) | (cl_Ball (p,r))) | Br,((TOP-REAL n) | (cl_Ball (q,s))) | Bs are_homeomorphic by A4, METRIZTS:3, METRIZTS:def 1;

then (TOP-REAL n) | (Ball (p,r)),((TOP-REAL n) | (cl_Ball (q,s))) | Bs are_homeomorphic by PRE_TOPC:7, A8;

hence Tball (p,r), Tball (q,s) are_homeomorphic by PRE_TOPC:7, A5; :: thesis: verum