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_{1}[ 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_{1}[u,y]

A3: for x being Point of (Tunit_circle n) holds S_{1}[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

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

( 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

proof

consider f being Function of (Tunit_circle n),(Tcircle (x,r)) such that
let u be Point of (Tunit_circle n); :: thesis: ex y being Point of (Tcircle (x,r)) st S_{1}[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_{1}[u,y]

thus S_{1}[u,y]
; :: thesis: verum

end;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

thus S

A3: for x being Point of (Tunit_circle n) holds S

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

hence
f is being_homeomorphism
by Th19; :: thesis: verum
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_{1}[a,f . a]
by A3;

hence ( a = b implies f . a = (r * b) + x ) ; :: thesis: verum

end;f . a = (r * b) + x

let b be Point of (TOP-REAL n); :: thesis: ( a = b implies f . a = (r * b) + x )

S

hence ( a = b implies f . a = (r * b) + x ) ; :: thesis: verum