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

per cases ( n is empty or not n is empty ) ;

suppose A1: n is empty ; :: thesis: Tball (p,r), Tball (q,s) are_homeomorphic

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p, q1 = q as Point of (TOP-REAL n1) ;
set X = { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } ;
set Y = { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } ;
A2: p1 = 0. (TOP-REAL 0) by A1;
A3: q1 = 0. (TOP-REAL 0) by A1;
for x being set holds
( x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } iff x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } )

proof

let x be set ; :: thesis: ( x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } iff x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } )

hereby :: thesis: ( x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } implies x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } )

assume x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } ; :: thesis: x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s }
then consider x1 being Point of (TOP-REAL n) such that
A4: ( x = x1 & |.(x1 - p).| < r ) ;
reconsider x1 = x1 as Point of (TOP-REAL n1) ;
x1 = 0. (TOP-REAL 0) by A1;
then |.(x1 - p1).| = 0 by A2, TOPRNS_1:28;
hence x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } by A2, A3, A4; :: thesis: verum

end;

assume x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } ; :: thesis: x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r }
then consider x1 being Point of (TOP-REAL n) such that
A5: ( x = x1 & |.(x1 - q).| < s ) ;
reconsider x1 = x1 as Point of (TOP-REAL n1) ;
x1 = 0. (TOP-REAL 0) by A1;
then |.(x1 - q1).| = 0 by A3, TOPRNS_1:28;
hence x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } by A2, A3, A5; :: thesis: verum

end;

hence Tball (p,r), Tball (q,s) are_homeomorphic by TARSKI:1; :: thesis: verum

end;

suppose not n is empty ; :: thesis: Tball (p,r), Tball (q,s) are_homeomorphic

then reconsider n1 = n as non empty Element of NAT by ORDINAL1:def 12;
A6: for r being real positive number
for x being Point of (TOP-REAL n1) holds Tunit_ball n1, Tball (x,r) are_homeomorphic

proof

let r be real positive number ; :: thesis: for x being Point of (TOP-REAL n1) holds Tunit_ball n1, Tball (x,r) are_homeomorphic
let x be Point of (TOP-REAL n1); :: thesis: Tunit_ball n1, Tball (x,r) are_homeomorphic
set U = Tunit_ball n;
set C = Tball (x,r);
defpred S₁[ Point of (Tunit_ball n), set ] means ex w being Point of (TOP-REAL n1) st
( w = $1 & $2 = (r * w) + x );
A7: r is Real by XREAL_0:def 1;
A8: the carrier of (Tball (x,r)) = Ball (x,r) by Th4;
A9: for u being Point of (Tunit_ball n) ex y being Point of (Tball (x,r)) st S₁[u,y]

proof

let u be Point of (Tunit_ball n); :: thesis: ex y being Point of (Tball (x,r)) st S₁[u,y]
reconsider v = u as Point of (TOP-REAL n1) by PRE_TOPC:25;
set y = (r * v) + x;
A10: |.(((r * v) + x) - x).| = |.(r * v).| by EUCLID:48
.= (abs r) * |.v.| by A7, TOPRNS_1:7
.= r * |.v.| by ABSVALUE:def 1 ;
r * |.v.| < r * 1 by Th5, XREAL_1:68;
then reconsider y = (r * v) + x as Point of (Tball (x,r)) by A10, A8, TOPREAL9:7;
take y ; :: thesis: S₁[u,y]
thus S₁[u,y] ; :: thesis: verum

end;

consider f being Function of (Tunit_ball n),(Tball (x,r)) such that
A11: for x being Point of (Tunit_ball n) holds S₁[x,f . x] from FUNCT_2:sch 3(A9);
for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n1) st a = b holds
f . a = (r * b) + x

proof

let a be Point of (Tunit_ball n); :: thesis: for b being Point of (TOP-REAL n1) st a = b holds
f . a = (r * b) + x
let b be Point of (TOP-REAL n1); :: thesis: ( a = b implies f . a = (r * b) + x )
S₁[a,f . a] by A11;
hence ( a = b implies f . a = (r * b) + x ) ; :: thesis: verum

end;

then ex f being Function of (Tunit_ball n),(Tball (x,r)) st f is being_homeomorphism by Th7;
hence Tunit_ball n1, Tball (x,r) are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum

end;

for x, y being Point of (TOP-REAL n1) holds Tball (x,r), Tball (y,s) are_homeomorphic

proof

let x, y be Point of (TOP-REAL n1); :: thesis: Tball (x,r), Tball (y,s) are_homeomorphic
A12: Tunit_ball n, Tball (y,s) are_homeomorphic by A6;
Tball (x,r), Tunit_ball n are_homeomorphic by A6;
hence Tball (x,r), Tball (y,s) are_homeomorphic by A12, BORSUK_3:3; :: thesis: verum

end;

hence Tball (p,r), Tball (q,s) are_homeomorphic ; :: thesis: verum

end;

end;