let n be non empty Element of NAT ; :: thesis: for r being real positive number
for x being Point of (TOP-REAL n) holds Tunit_circle n, Tcircle x,r are_homeomorphic
let r be real positive number ; :: thesis: for x being Point of (TOP-REAL n) holds Tunit_circle n, Tcircle x,r are_homeomorphic
let x be Point of (TOP-REAL n); :: thesis: Tunit_circle n, Tcircle x,r are_homeomorphic
set U = Tunit_circle n;
set C = Tcircle x,r;
defpred S₁[ Point of (Tunit_circle n), set ] means ex w being Point of (TOP-REAL n) st
( w = $1 & $2 = (r * w) + x );
A1: r is Real by XREAL_0:def 1;
A2: the carrier of (Tcircle x,r) = Sphere x,r by Th9;
A3: for u being Point of (Tunit_circle n) ex y being Point of (Tcircle x,r) st S₁[u,y]

proof

let u be Point of (Tunit_circle n); :: thesis: ex y being Point of (Tcircle x,r) st S₁[u,y]
reconsider v = u as Point of (TOP-REAL n) by PRE_TOPC:55;
set y = (r * v) + x;
|.(((r * v) + x) - x).| = |.(r * v).| by EUCLID:52
.= (abs r) * |.v.| by A1, TOPRNS_1:8
.= r * |.v.| by ABSVALUE:def 1
.= r * 1 by Th12 ;
then reconsider y = (r * v) + x as Point of (Tcircle x,r) by A2, TOPREAL9:9;
take y ; :: thesis: S₁[u,y]
thus S₁[u,y] ; :: thesis: verum

end;

consider f being Function of (Tunit_circle n),(Tcircle x,r) such that
A4: for x being Point of (Tunit_circle n) holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
take f ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism
for a being Point of (Tunit_circle n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + x

proof

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

end;

hence f is being_homeomorphism by Th19; :: thesis: verum