let n be non zero Element of NAT ; :: thesis: for r being positive Real

for x being Point of (TOP-REAL n)

for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( 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 ) holds

f is being_homeomorphism

let r be positive Real; :: thesis: for x being Point of (TOP-REAL n)

for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( 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 ) holds

f is being_homeomorphism

let x be Point of (TOP-REAL n); :: thesis: for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( 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 ) holds

f is being_homeomorphism

let f be Function of (Tunit_circle n),(Tcircle (x,r)); :: thesis: ( ( 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 ) implies f is being_homeomorphism )

assume A1: 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 ; :: thesis: f is being_homeomorphism

defpred S_{1}[ Point of (TOP-REAL n), set ] means $2 = (r * $1) + x;

set U = Tunit_circle n;

set C = Tcircle (x,r);

A2: for u being Point of (TOP-REAL n) ex y being Point of (TOP-REAL n) st S_{1}[u,y]
;

consider F being Function of (TOP-REAL n),(TOP-REAL n) such that

A3: for x being Point of (TOP-REAL n) holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A2);

defpred S_{2}[ Point of (TOP-REAL n), set ] means $2 = (1 / r) * ($1 - x);

A4: for u being Point of (TOP-REAL n) ex y being Point of (TOP-REAL n) st S_{2}[u,y]
;

consider G being Function of (TOP-REAL n),(TOP-REAL n) such that

A5: for a being Point of (TOP-REAL n) holds S_{2}[a,G . a]
from FUNCT_2:sch 3(A4);

set f2 = (TOP-REAL n) --> x;

set f1 = id (TOP-REAL n);

dom G = the carrier of (TOP-REAL n) by FUNCT_2:def 1;

then A6: dom (G | (Sphere (x,r))) = Sphere (x,r) by RELAT_1:62;

for p being Point of (TOP-REAL n) holds G . p = ((1 / r) * ((id (TOP-REAL n)) . p)) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p))

thus dom f = [#] (Tunit_circle n) 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 (Tunit_circle n) by FUNCT_2:def 1;

for p being Point of (TOP-REAL n) holds F . p = (r * ((id (TOP-REAL n)) . p)) + (1 * (((TOP-REAL n) --> x) . p))

A10: the carrier of (Tcircle (x,r)) = Sphere (x,r) by Th9;

A11: the carrier of (Tunit_circle n) = Sphere ((0. (TOP-REAL n)),1) by Th9;

A12: for a being object st a in dom f holds

f . a = (F | (Sphere ((0. (TOP-REAL n)),1))) . a

thus A15: rng f = [#] (Tcircle (x,r)) :: thesis: ( f is one-to-one & f is continuous & f /" is continuous )

(f ") . a = (G | (Sphere (x,r))) . a

then dom (F | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by RELAT_1:62;

hence f is continuous by A11, A8, A9, A12, BORSUK_4:44, FUNCT_1:2; :: thesis: f /" is continuous

dom (f ") = the carrier of (Tcircle (x,r)) by FUNCT_2:def 1;

hence f /" is continuous by A10, A6, A7, A23, BORSUK_4:44, FUNCT_1:2; :: thesis: verum

for x being Point of (TOP-REAL n)

for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( 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 ) holds

f is being_homeomorphism

let r be positive Real; :: thesis: for x being Point of (TOP-REAL n)

for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( 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 ) holds

f is being_homeomorphism

let x be Point of (TOP-REAL n); :: thesis: for f being Function of (Tunit_circle n),(Tcircle (x,r)) st ( 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 ) holds

f is being_homeomorphism

let f be Function of (Tunit_circle n),(Tcircle (x,r)); :: thesis: ( ( 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 ) implies f is being_homeomorphism )

assume A1: 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 ; :: thesis: f is being_homeomorphism

defpred S

set U = Tunit_circle n;

set C = Tcircle (x,r);

A2: for u being Point of (TOP-REAL n) ex y being Point of (TOP-REAL n) st S

consider F being Function of (TOP-REAL n),(TOP-REAL n) such that

A3: for x being Point of (TOP-REAL n) holds S

defpred S

A4: for u being Point of (TOP-REAL n) ex y being Point of (TOP-REAL n) st S

consider G being Function of (TOP-REAL n),(TOP-REAL n) such that

A5: for a being Point of (TOP-REAL n) holds S

set f2 = (TOP-REAL n) --> x;

set f1 = id (TOP-REAL n);

dom G = the carrier of (TOP-REAL n) by FUNCT_2:def 1;

then A6: dom (G | (Sphere (x,r))) = Sphere (x,r) by RELAT_1:62;

for p being Point of (TOP-REAL n) holds G . p = ((1 / r) * ((id (TOP-REAL n)) . p)) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p))

proof

then A7:
G is continuous
by TOPALG_1:16;
let p be Point of (TOP-REAL n); :: thesis: G . p = ((1 / r) * ((id (TOP-REAL n)) . p)) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p))

thus ((1 / r) * ((id (TOP-REAL n)) . p)) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p)) = ((1 / r) * p) + ((- (1 / r)) * (((TOP-REAL n) --> 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;thus ((1 / r) * ((id (TOP-REAL n)) . p)) + ((- (1 / r)) * (((TOP-REAL n) --> x) . p)) = ((1 / r) * p) + ((- (1 / r)) * (((TOP-REAL n) --> 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

thus dom f = [#] (Tunit_circle n) 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 (Tunit_circle n) by FUNCT_2:def 1;

for p being Point of (TOP-REAL n) holds F . p = (r * ((id (TOP-REAL n)) . p)) + (1 * (((TOP-REAL n) --> x) . p))

proof

then A9:
F is continuous
by TOPALG_1:16;
let p be Point of (TOP-REAL n); :: thesis: F . p = (r * ((id (TOP-REAL n)) . p)) + (1 * (((TOP-REAL n) --> x) . p))

thus (r * ((id (TOP-REAL n)) . p)) + (1 * (((TOP-REAL n) --> x) . p)) = (r * ((id (TOP-REAL n)) . p)) + (((TOP-REAL n) --> x) . p) by RLVECT_1:def 8

.= (r * p) + (((TOP-REAL n) --> x) . p)

.= (r * p) + x

.= F . p by A3 ; :: thesis: verum

end;thus (r * ((id (TOP-REAL n)) . p)) + (1 * (((TOP-REAL n) --> x) . p)) = (r * ((id (TOP-REAL n)) . p)) + (((TOP-REAL n) --> x) . p) by RLVECT_1:def 8

.= (r * p) + (((TOP-REAL n) --> x) . p)

.= (r * p) + x

.= F . p by A3 ; :: thesis: verum

A10: the carrier of (Tcircle (x,r)) = Sphere (x,r) by Th9;

A11: the carrier of (Tunit_circle n) = Sphere ((0. (TOP-REAL n)),1) by Th9;

A12: for a being object st a in dom f holds

f . a = (F | (Sphere ((0. (TOP-REAL n)),1))) . a

proof

A14:
(1 / r) * r = 1
by XCMPLX_1:87;
let a be object ; :: thesis: ( a in dom f implies f . a = (F | (Sphere ((0. (TOP-REAL n)),1))) . a )

assume A13: a in dom f ; :: thesis: f . a = (F | (Sphere ((0. (TOP-REAL n)),1))) . a

reconsider y = a as Point of (TOP-REAL n) by A13, PRE_TOPC:25;

thus f . a = (r * y) + x by A1, A13

.= F . y by A3

.= (F | (Sphere ((0. (TOP-REAL n)),1))) . a by A11, A13, FUNCT_1:49 ; :: thesis: verum

end;assume A13: a in dom f ; :: thesis: f . a = (F | (Sphere ((0. (TOP-REAL n)),1))) . a

reconsider y = a as Point of (TOP-REAL n) by A13, PRE_TOPC:25;

thus f . a = (r * y) + x by A1, A13

.= F . y by A3

.= (F | (Sphere ((0. (TOP-REAL n)),1))) . a by A11, A13, FUNCT_1:49 ; :: thesis: verum

thus A15: rng f = [#] (Tcircle (x,r)) :: thesis: ( f is one-to-one & f is continuous & f /" is continuous )

proof

thus A18:
f is one-to-one
:: thesis: ( f is continuous & f /" is continuous )
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 (TOP-REAL n) by PRE_TOPC:25;

set a = (1 / r) * (c - x);

|.(((1 / r) * (c - x)) - (0. (TOP-REAL n))).| = |.((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 A10, A16, TOPREAL9:9 ;

then A17: (1 / r) * (c - x) in Sphere ((0. (TOP-REAL n)),1) by A14;

then f . ((1 / r) * (c - x)) = (r * ((1 / r) * (c - x))) + x by A1, A11

.= ((r * (1 / r)) * (c - x)) + x by RLVECT_1:def 7

.= (c - x) + x by A14, RLVECT_1:def 8

.= b by RLVECT_4:1 ;

hence b in rng f by A11, A8, A17, FUNCT_1:def 3; :: thesis: verum

end;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 (TOP-REAL n) by PRE_TOPC:25;

set a = (1 / r) * (c - x);

|.(((1 / r) * (c - x)) - (0. (TOP-REAL n))).| = |.((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 A10, A16, TOPREAL9:9 ;

then A17: (1 / r) * (c - x) in Sphere ((0. (TOP-REAL n)),1) by A14;

then f . ((1 / r) * (c - x)) = (r * ((1 / r) * (c - x))) + x by A1, A11

.= ((r * (1 / r)) * (c - x)) + x by RLVECT_1:def 7

.= (c - x) + x by A14, RLVECT_1:def 8

.= b by RLVECT_4:1 ;

hence b in rng f by A11, A8, A17, FUNCT_1:def 3; :: thesis: verum

proof

A23:
for a being object st a in dom (f ") holds
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 (TOP-REAL n) by A11, A8, A19, A20;

A22: f . b1 = (r * b1) + x by A1, A20;

f . a1 = (r * a1) + x by A1, A19;

then r * a1 = ((r * b1) + x) - x by A21, A22, RLVECT_4:1;

hence a = b by RLVECT_1:36, RLVECT_4:1; :: thesis: verum

end;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 (TOP-REAL n) by A11, A8, A19, A20;

A22: f . b1 = (r * b1) + x by A1, A20;

f . a1 = (r * a1) + x by A1, A19;

then r * a1 = ((r * b1) + x) - x by A21, A22, RLVECT_4:1;

hence a = b by RLVECT_1:36, RLVECT_4:1; :: thesis: verum

(f ") . a = (G | (Sphere (x,r))) . a

proof

dom F = the carrier of (TOP-REAL n)
by FUNCT_2:def 1;
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 (TOP-REAL n) by A24, PRE_TOPC:25;

set e = (1 / r) * (y - x);

A25: f is onto by A15;

|.(((1 / r) * (y - x)) - (0. (TOP-REAL n))).| = |.((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 A10, A24, TOPREAL9:9 ;

then A26: (1 / r) * (y - x) in Sphere ((0. (TOP-REAL n)),1) by A14;

then f . ((1 / r) * (y - x)) = (r * ((1 / r) * (y - x))) + x by A1, A11

.= ((r * (1 / r)) * (y - x)) + x by RLVECT_1:def 7

.= (y - x) + x by A14, RLVECT_1:def 8

.= y by RLVECT_4:1 ;

then (ff ") . a = (1 / r) * (y - x) by A11, A8, A18, A26, FUNCT_1:32;

hence (f ") . a = (1 / r) * (y - x) by A25, A18, TOPS_2:def 4

.= G . y by A5

.= (G | (Sphere (x,r))) . a by A10, A24, FUNCT_1:49 ;

:: thesis: verum

end;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 (TOP-REAL n) by A24, PRE_TOPC:25;

set e = (1 / r) * (y - x);

A25: f is onto by A15;

|.(((1 / r) * (y - x)) - (0. (TOP-REAL n))).| = |.((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 A10, A24, TOPREAL9:9 ;

then A26: (1 / r) * (y - x) in Sphere ((0. (TOP-REAL n)),1) by A14;

then f . ((1 / r) * (y - x)) = (r * ((1 / r) * (y - x))) + x by A1, A11

.= ((r * (1 / r)) * (y - x)) + x by RLVECT_1:def 7

.= (y - x) + x by A14, RLVECT_1:def 8

.= y by RLVECT_4:1 ;

then (ff ") . a = (1 / r) * (y - x) by A11, A8, A18, A26, FUNCT_1:32;

hence (f ") . a = (1 / r) * (y - x) by A25, A18, TOPS_2:def 4

.= G . y by A5

.= (G | (Sphere (x,r))) . a by A10, A24, FUNCT_1:49 ;

:: thesis: verum

then dom (F | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by RELAT_1:62;

hence f is continuous by A11, A8, A9, A12, BORSUK_4:44, FUNCT_1:2; :: thesis: f /" is continuous

dom (f ") = the carrier of (Tcircle (x,r)) by FUNCT_2:def 1;

hence f /" is continuous by A10, A6, A7, A23, BORSUK_4:44, FUNCT_1:2; :: thesis: verum