let n be natural number ; :: thesis: for p being Point of (TOP-REAL n)
for r being real positive number
for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) holds
f is being_homeomorphism
let p be Point of (TOP-REAL n); :: thesis: for r being real positive number
for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) holds
f is being_homeomorphism
let r be real positive number ; :: thesis: for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) holds
f is being_homeomorphism
let f be Function of (Tunit_ball n),(Tball (p,r)); :: thesis: ( n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) implies f is being_homeomorphism )
assume that
A1: n <> 0 and
A2: for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ; :: thesis: f is being_homeomorphism
reconsider n1 = n as non empty Element of NAT by A1, ORDINAL1:def 12;
reconsider x = p as Point of (TOP-REAL n1) ;
defpred S₁[ Point of (TOP-REAL n1), set ] means $2 = (r * $1) + x;
set U = Tunit_ball n;
set B = Tball (x,r);
A3: for u being Point of (TOP-REAL n1) ex y being Point of (TOP-REAL n1) st S₁[u,y] ;
consider F being Function of (TOP-REAL n1),(TOP-REAL n1) such that
A4: for x being Point of (TOP-REAL n1) holds S₁[x,F . x] from FUNCT_2:sch 3(A3);
defpred S₂[ Point of (TOP-REAL n1), set ] means $2 = (1 / r) * ($1 - x);
A5: for u being Point of (TOP-REAL n1) ex y being Point of (TOP-REAL n1) st S₂[u,y] ;
consider G being Function of (TOP-REAL n1),(TOP-REAL n1) such that
A6: for a being Point of (TOP-REAL n1) holds S₂[a,G . a] from FUNCT_2:sch 3(A5);
set f2 = (TOP-REAL n1) --> x;
set f1 = id (TOP-REAL n1);
dom G = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
then A7: dom (G | (Ball (x,r))) = Ball (x,r) by RELAT_1:62;
for p being Point of (TOP-REAL n1) holds G . p = ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p))

proof

let p be Point of (TOP-REAL n1); :: thesis: G . p = ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p))
thus ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p)) = ((1 / r) * p) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p)) by FUNCT_1:18
.= ((1 / r) * p) + ((- (1 / r)) * x) by FUNCOP_1:7
.= ((1 / r) * p) - ((1 / r) * x) by EUCLID:40
.= (1 / r) * (p - x) by EUCLID:49
.= G . p by A6 ; :: thesis: verum

end;

then A8: G is continuous by TOPALG_1:16;
A9: dom f = [#] (Tunit_ball n) by FUNCT_2:def 1;
A10: dom f = the carrier of (Tunit_ball n) by FUNCT_2:def 1;
for p being Point of (TOP-REAL n1) holds F . p = (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p))

proof

let p be Point of (TOP-REAL n1); :: thesis: F . p = (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p))
thus (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p)) = (r * ((id (TOP-REAL n1)) . p)) + (((TOP-REAL n1) --> x) . p) by EUCLID:29
.= (r * p) + (((TOP-REAL n1) --> x) . p) by FUNCT_1:18
.= (r * p) + x by FUNCOP_1:7
.= F . p by A4 ; :: thesis: verum

end;

then A11: F is continuous by TOPALG_1:16;
A12: the carrier of (Tball (x,r)) = Ball (x,r) by Th4;
A13: the carrier of (Tunit_ball n) = Ball ((0. (TOP-REAL n)),1) by Th4;
A14: for a being set st a in dom f holds
f . a = (F | (Ball ((0. (TOP-REAL n)),1))) . a

proof

let a be set ; :: thesis: ( a in dom f implies f . a = (F | (Ball ((0. (TOP-REAL n)),1))) . a )
assume A15: a in dom f ; :: thesis: f . a = (F | (Ball ((0. (TOP-REAL n)),1))) . a
reconsider y = a as Point of (TOP-REAL n1) by A15, PRE_TOPC:25;
thus f . a = (r * y) + x by A2, A15
.= F . y by A4
.= (F | (Ball ((0. (TOP-REAL n)),1))) . a by A13, A15, FUNCT_1:49 ; :: thesis: verum

end;

A16: (1 / r) * r = 1 by XCMPLX_1:87;
A17: rng f = [#] (Tball (x,r))

proof

now

let b be set ; :: thesis: ( b in [#] (Tball (x,r)) implies b in rng f )
assume A18: b in [#] (Tball (x,r)) ; :: thesis: b in rng f
then reconsider c = b as Point of (TOP-REAL n1) by PRE_TOPC:25;
reconsider r1 = 1 / r as Real ;
set a = r1 * (c - x);
A19: |.((r1 * (c - x)) - (0. (TOP-REAL n1))).| = |.(r1 * (c - x)).| by RLVECT_1:13
.= (abs r1) * |.(c - x).| by TOPRNS_1:7
.= r1 * |.(c - x).| by ABSVALUE:def 1 ;
|.(c - x).| < r by A12, A18, TOPREAL9:7;
then (1 / r) * |.(c - x).| < (1 / r) * r by XREAL_1:68;
then A20: r1 * (c - x) in Ball ((0. (TOP-REAL n)),1) by A16, A19;
then f . (r1 * (c - x)) = (r * (r1 * (c - x))) + x by A2, A13
.= ((r * (1 / r)) * (c - x)) + x by EUCLID:30
.= (c - x) + x by A16, EUCLID:29
.= b by EUCLID:48 ;
hence b in rng f by A13, A10, A20, FUNCT_1:def 3; :: thesis: verum

end;

then [#] (Tball (x,r)) c= rng f by TARSKI:def 3;
hence rng f = [#] (Tball (x,r)) by XBOOLE_0:def 10; :: thesis: verum

end;

now

let a, b be set ; :: thesis: ( a in dom f & b in dom f & f . a = f . b implies a = b )
assume that
A21: a in dom f and
A22: b in dom f and
A23: f . a = f . b ; :: thesis: a = b
reconsider a1 = a, b1 = b as Point of (TOP-REAL n1) by A13, A10, A21, A22;
A24: f . b1 = (r * b1) + x by A2, A22;
f . a1 = (r * a1) + x by A2, A21;
then r * a1 = ((r * b1) + x) - x by A23, A24, EUCLID:48;
hence a = b by EUCLID:34, EUCLID:48; :: thesis: verum

end;

then A25: f is one-to-one by FUNCT_1:def 4;
A26: for a being set st a in dom (f ") holds
(f ") . a = (G | (Ball (x,r))) . a

proof

reconsider ff = f as Function ;
let a be set ; :: thesis: ( a in dom (f ") implies (f ") . a = (G | (Ball (x,r))) . a )
assume A27: a in dom (f ") ; :: thesis: (f ") . a = (G | (Ball (x,r))) . a
reconsider y = a as Point of (TOP-REAL n1) by A27, PRE_TOPC:25;
reconsider r1 = 1 / r as Real ;
set e = (1 / r) * (y - x);
B1: f is onto by A17, FUNCT_2:def 3;
A28: |.(((1 / r) * (y - x)) - (0. (TOP-REAL n1))).| = |.((1 / r) * (y - x)).| by RLVECT_1:13
.= (abs r1) * |.(y - x).| by TOPRNS_1:7
.= r1 * |.(y - x).| by ABSVALUE:def 1 ;
|.(y - x).| < r by A27, A12, TOPREAL9:7;
then (1 / r) * |.(y - x).| < (1 / r) * r by XREAL_1:68;
then A29: (1 / r) * (y - x) in Ball ((0. (TOP-REAL n)),1) by A16, A28;
then f . ((1 / r) * (y - x)) = (r * ((1 / r) * (y - x))) + x by A2, A13
.= ((r * (1 / r)) * (y - x)) + x by EUCLID:30
.= (y - x) + x by A16, EUCLID:29
.= y by EUCLID:48 ;
then (ff ") . a = (1 / r) * (y - x) by A13, A10, A25, A29, FUNCT_1:32;
hence (f ") . a = (1 / r) * (y - x) by B1, A25, TOPS_2:def 4
.= G . y by A6
.= (G | (Ball (x,r))) . a by A12, A27, FUNCT_1:49 ;
:: thesis: verum

end;

dom F = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
then dom (F | (Ball ((0. (TOP-REAL n)),1))) = Ball ((0. (TOP-REAL n)),1) by RELAT_1:62;
then A30: f is continuous by A13, A10, A11, A14, BORSUK_4:44, FUNCT_1:2;
A31: dom (f ") = the carrier of (Tball (x,r)) by FUNCT_2:def 1;
f " is continuous by A31, A12, A7, A8, A26, BORSUK_4:44, FUNCT_1:2;
hence f is being_homeomorphism by A9, A17, A25, A30, TOPS_2:def 5; :: thesis: verum