let n be non zero Element of NAT ; :: thesis: for r being positive Real
for x being Point of ()
for f being Function of (),(Tcircle (x,r)) st ( for a being Point of ()
for b being Point of () st a = b holds
f . a = (r * b) + x ) holds
f is being_homeomorphism

let r be positive Real; :: thesis: for x being Point of ()
for f being Function of (),(Tcircle (x,r)) st ( for a being Point of ()
for b being Point of () st a = b holds
f . a = (r * b) + x ) holds
f is being_homeomorphism

let x be Point of (); :: thesis: for f being Function of (),(Tcircle (x,r)) st ( for a being Point of ()
for b being Point of () st a = b holds
f . a = (r * b) + x ) holds
f is being_homeomorphism

let f be Function of (),(Tcircle (x,r)); :: thesis: ( ( for a being Point of ()
for b being Point of () st a = b holds
f . a = (r * b) + x ) implies f is being_homeomorphism )

assume A1: for a being Point of ()
for b being Point of () st a = b holds
f . a = (r * b) + x ; :: thesis:
defpred S1[ Point of (), set ] means \$2 = (r * \$1) + x;
set U = Tunit_circle n;
set C = Tcircle (x,r);
A2: for u being Point of () ex y being Point of () st S1[u,y] ;
consider F being Function of (),() such that
A3: for x being Point of () holds S1[x,F . x] from defpred S2[ Point of (), set ] means \$2 = (1 / r) * (\$1 - x);
A4: for u being Point of () ex y being Point of () st S2[u,y] ;
consider G being Function of (),() such that
A5: for a being Point of () holds S2[a,G . a] from set f2 = () --> x;
set f1 = id ();
dom G = the carrier of () by FUNCT_2:def 1;
then A6: dom (G | (Sphere (x,r))) = Sphere (x,r) by RELAT_1:62;
for p being Point of () holds G . p = ((1 / r) * ((id ()) . p)) + ((- (1 / r)) * ((() --> x) . p))
proof
let p be Point of (); :: thesis: G . p = ((1 / r) * ((id ()) . p)) + ((- (1 / r)) * ((() --> x) . p))
thus ((1 / r) * ((id ()) . p)) + ((- (1 / r)) * ((() --> x) . p)) = ((1 / r) * p) + ((- (1 / r)) * ((() --> x) . p))
.= ((1 / r) * p) + ((- (1 / r)) * x)
.= ((1 / r) * p) - ((1 / r) * x) by RLVECT_1:79
.= (1 / r) * (p - x) by RLVECT_1:34
.= G . p by A5 ; :: thesis: verum
end;
then A7: G is continuous by TOPALG_1:16;
thus dom f = [#] () by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng f = [#] (Tcircle (x,r)) & f is one-to-one & f is continuous & f /" is continuous )
A8: dom f = the carrier of () by FUNCT_2:def 1;
for p being Point of () holds F . p = (r * ((id ()) . p)) + (1 * ((() --> x) . p))
proof
let p be Point of (); :: thesis: F . p = (r * ((id ()) . p)) + (1 * ((() --> x) . p))
thus (r * ((id ()) . p)) + (1 * ((() --> x) . p)) = (r * ((id ()) . p)) + ((() --> x) . p) by RLVECT_1:def 8
.= (r * p) + ((() --> x) . p)
.= (r * p) + x
.= F . p by A3 ; :: thesis: verum
end;
then A9: F is continuous by TOPALG_1:16;
A10: the carrier of (Tcircle (x,r)) = Sphere (x,r) by Th9;
A11: the carrier of () = Sphere ((0. ()),1) by Th9;
A12: for a being object st a in dom f holds
f . a = (F | (Sphere ((0. ()),1))) . a
proof
let a be object ; :: thesis: ( a in dom f implies f . a = (F | (Sphere ((0. ()),1))) . a )
assume A13: a in dom f ; :: thesis: f . a = (F | (Sphere ((0. ()),1))) . a
reconsider y = a as Point of () by ;
thus f . a = (r * y) + x by
.= F . y by A3
.= (F | (Sphere ((0. ()),1))) . a by ; :: thesis: verum
end;
A14: (1 / r) * r = 1 by XCMPLX_1:87;
thus A15: rng f = [#] (Tcircle (x,r)) :: thesis: ( f is one-to-one & f is continuous & f /" is continuous )
proof
thus rng f c= [#] (Tcircle (x,r)) ; :: according to XBOOLE_0:def 10 :: thesis: [#] (Tcircle (x,r)) c= rng f
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in [#] (Tcircle (x,r)) or b in rng f )
assume A16: b in [#] (Tcircle (x,r)) ; :: thesis: b in rng f
then reconsider c = b as Point of () by PRE_TOPC:25;
set a = (1 / r) * (c - x);
|.(((1 / r) * (c - x)) - (0. ())).| = |.((1 / r) * (c - x)).| by RLVECT_1:13
.= |.(1 / r).| * |.(c - x).| by TOPRNS_1:7
.= (1 / r) * |.(c - x).| by ABSVALUE:def 1
.= (1 / r) * r by ;
then A17: (1 / r) * (c - x) in Sphere ((0. ()),1) by A14;
then f . ((1 / r) * (c - x)) = (r * ((1 / r) * (c - x))) + x by
.= ((r * (1 / r)) * (c - x)) + x by RLVECT_1:def 7
.= (c - x) + x by
.= b by RLVECT_4:1 ;
hence b in rng f by ; :: thesis: verum
end;
thus A18: f is one-to-one :: thesis: ( f is continuous & f /" is continuous )
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in K112(f) or not b in K112(f) or not f . a = f . b or a = b )
assume that
A19: a in dom f and
A20: b in dom f and
A21: f . a = f . b ; :: thesis: a = b
reconsider a1 = a, b1 = b as Point of () by A11, A8, A19, A20;
A22: f . b1 = (r * b1) + x by ;
f . a1 = (r * a1) + x by ;
then r * a1 = ((r * b1) + x) - x by ;
hence a = b by ; :: thesis: verum
end;
A23: for a being object st a in dom (f ") holds
(f ") . a = (G | (Sphere (x,r))) . a
proof
reconsider ff = f as Function ;
let a be object ; :: thesis: ( a in dom (f ") implies (f ") . a = (G | (Sphere (x,r))) . a )
assume A24: a in dom (f ") ; :: thesis: (f ") . a = (G | (Sphere (x,r))) . a
reconsider y = a as Point of () by ;
set e = (1 / r) * (y - x);
A25: f is onto by A15;
|.(((1 / r) * (y - x)) - (0. ())).| = |.((1 / r) * (y - x)).| by RLVECT_1:13
.= |.(1 / r).| * |.(y - x).| by TOPRNS_1:7
.= (1 / r) * |.(y - x).| by ABSVALUE:def 1
.= (1 / r) * r by ;
then A26: (1 / r) * (y - x) in Sphere ((0. ()),1) by A14;
then f . ((1 / r) * (y - x)) = (r * ((1 / r) * (y - x))) + x by
.= ((r * (1 / r)) * (y - x)) + x by RLVECT_1:def 7
.= (y - x) + x by
.= y by RLVECT_4:1 ;
then (ff ") . a = (1 / r) * (y - x) by ;
hence (f ") . a = (1 / r) * (y - x) by
.= G . y by A5
.= (G | (Sphere (x,r))) . a by ;
:: thesis: verum
end;
dom F = the carrier of () by FUNCT_2:def 1;
then dom (F | (Sphere ((0. ()),1))) = Sphere ((0. ()),1) by RELAT_1:62;
hence f is continuous by ; :: thesis: f /" is continuous
dom (f ") = the carrier of (Tcircle (x,r)) by FUNCT_2:def 1;
hence f /" is continuous by ; :: thesis: verum