let n be non zero Element of NAT ; :: thesis: for r being positive Real
for x being Point of (TOP-REAL n) holds Tunit_circle n, Tcircle (x,r) are_homeomorphic
let r be positive Real; :: 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: the carrier of (Tcircle (x,r)) = Sphere (x,r) by Th9;
A2: 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:25;
set y = (r * v) + x;
|.(((r * v) + x) - x).| = |.(r * v).| by RLVECT_4:1
.= |.r.| * |.v.| by TOPRNS_1:7
.= r * |.v.| by ABSVALUE:def 1
.= r * 1 by Th12 ;
then reconsider y = (r * v) + x as Point of (Tcircle (x,r)) by A1, 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
A3: for x being Point of (Tunit_circle n) holds S₁[x,f . x] from FUNCT_2:sch 3(A2);
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 A3;
hence ( a = b implies f . a = (r * b) + x ) ; :: thesis: verum

end;

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