let n be non zero Element of NAT ; 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; 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); Tunit_circle n, Tcircle (x,r) are_homeomorphic
set U = Tunit_circle n;
set C = Tcircle (x,r);
defpred S1[ 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 S1[u,y]
consider f being Function of (Tunit_circle n),(Tcircle (x,r)) such that
A3:
for x being Point of (Tunit_circle n) holds S1[x,f . x]
from FUNCT_2:sch 3(A2);
take
f
; T_0TOPSP:def 1 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
hence
f is being_homeomorphism
by Th19; verum