let n be non zero Element of NAT ; :: thesis: for r being positive Real
for x being Point of () holds Tunit_circle n, Tcircle (x,r) are_homeomorphic

let r be positive Real; :: thesis: for x being Point of () holds Tunit_circle n, Tcircle (x,r) are_homeomorphic
let x be Point of (); :: thesis:
set U = Tunit_circle n;
set C = Tcircle (x,r);
defpred S1[ Point of (), set ] means ex w being Point of () 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 () ex y being Point of (Tcircle (x,r)) st S1[u,y]
proof
let u be Point of (); :: thesis: ex y being Point of (Tcircle (x,r)) st S1[u,y]
reconsider v = u as Point of () 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 ;
take y ; :: thesis: S1[u,y]
thus S1[u,y] ; :: thesis: verum
end;
consider f being Function of (),(Tcircle (x,r)) such that
A3: for x being Point of () holds S1[x,f . x] from take f ; :: according to T_0TOPSP:def 1 :: thesis:
for a being Point of ()
for b being Point of () st a = b holds
f . a = (r * b) + x
proof
let a be Point of (); :: thesis: for b being Point of () st a = b holds
f . a = (r * b) + x

let b be Point of (); :: thesis: ( a = b implies f . a = (r * b) + x )
S1[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