let n be Nat; :: thesis: for f being Function of (Tunit_ball n),(TOP-REAL n) 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 = (1 / (1 - (|.b.| * |.b.|))) * b ) holds
f is being_homeomorphism
let f be Function of (Tunit_ball n),(TOP-REAL n); :: 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 = (1 / (1 - (|.b.| * |.b.|))) * b ) 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 = (1 / (1 - (|.b.| * |.b.|))) * b ; :: thesis: f is being_homeomorphism
A3: dom f = [#] (Tunit_ball n) by FUNCT_2:def 1;
A4: [#] (Tunit_ball n) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;
reconsider n1 = n as non zero Element of NAT by A1, ORDINAL1:def 12;
for y being object st y in [#] (TOP-REAL n1) holds
ex x being object st [x,y] in f then A14: rng f = [#] (TOP-REAL n1) by RELSET_1:10;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 then A34: f is one-to-one ;
consider f0 being Function of (TOP-REAL n1),R^1 such that
A35: ( ( for p being Point of (TOP-REAL n1) holds f0 . p = 1 ) & f0 is continuous ) by JGRAPH_2:20;
consider f1 being Function of (TOP-REAL n1),R^1 such that
A36: ( ( for p being Point of (TOP-REAL n1) holds f1 . p = |.p.| ) & f1 is continuous ) by JORDAN2C:84;
consider f2 being Function of (TOP-REAL n),R^1 such that
A37: ( ( for p being Point of (TOP-REAL n)
for r1 being Real st f1 . p = r1 holds
f2 . p = r1 * r1 ) & f2 is continuous ) by A36, JGRAPH_2:22;
consider f3 being Function of (TOP-REAL n),R^1 such that
A38: ( ( for p being Point of (TOP-REAL n)
for r1, r2 being Real st f0 . p = r1 & f2 . p = r2 holds
f3 . p = r1 - r2 ) & f3 is continuous ) by A35, A37, JGRAPH_2:21;
reconsider f3 = f3 as continuous Function of (TOP-REAL n),R^1 by A38;
A39: for p being Point of (TOP-REAL n) holds f3 . p = 1 - (|.p.| * |.p.|) set f4 = f3 | (Tunit_ball n);
for p being Point of (Tunit_ball n) holds (f3 | (Tunit_ball n)) . p <> 0 then consider f5 being Function of (Tunit_ball n),R^1 such that
A42: ( ( for p being Point of (Tunit_ball n)
for r1 being Real st (f3 | (Tunit_ball n)) . p = r1 holds
f5 . p = 1 / r1 ) & f5 is continuous ) by JGRAPH_2:26;
consider f6 being Function of (Tunit_ball n),(TOP-REAL n) such that
A43: ( ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n)
for r being Real st a = b & f5 . a = r holds
f6 . b = r * b ) & f6 is continuous ) by A42, Th2;
A44: dom f = the carrier of (Tunit_ball n) by FUNCT_2:def 1
.= dom f6 by FUNCT_2:def 1 ;
for x being object st x in dom f holds
f . x = f6 . x then A47: f = f6 by A44;
consider f8 being Function of (TOP-REAL n),R^1 such that
A48: ( ( for p being Point of (TOP-REAL n)
for r1 being Real st f2 . p = r1 holds
f8 . p = 4 * r1 ) & f8 is continuous ) by A37, JGRAPH_2:23;
consider f9 being Function of (TOP-REAL n),R^1 such that
A49: ( ( for p being Point of (TOP-REAL n)
for r1, r2 being Real st f0 . p = r1 & f8 . p = r2 holds
f9 . p = r1 + r2 ) & f9 is continuous ) by A48, A35, JGRAPH_2:19;
A50: for p being Point of (TOP-REAL n) holds f9 . p = 1 + ((4 * |.p.|) * |.p.|) A51: for p being Point of (TOP-REAL n) ex r being Real st
( f9 . p = r & r >= 0 ) consider f10 being Function of (TOP-REAL n),R^1 such that
A52: ( ( for p being Point of (TOP-REAL n)
for r1 being Real st f9 . p = r1 holds
f10 . p = sqrt r1 ) & f10 is continuous ) by A51, A49, JGRAPH_3:5;
consider f11 being Function of (TOP-REAL n),R^1 such that
A53: ( ( for p being Point of (TOP-REAL n)
for r1, r2 being Real st f0 . p = r1 & f10 . p = r2 holds
f11 . p = r1 + r2 ) & f11 is continuous ) by A52, A35, JGRAPH_2:19;
for p being Point of (TOP-REAL n) holds f11 . p <> 0 then consider f12 being Function of (TOP-REAL n),R^1 such that
A56: ( ( for p being Point of (TOP-REAL n)
for r1 being Real st f11 . p = r1 holds
f12 . p = 1 / r1 ) & f12 is continuous ) by A53, JGRAPH_2:26;
consider f13 being Function of (TOP-REAL n),R^1 such that
A57: ( ( for p being Point of (TOP-REAL n)
for r1 being Real st f12 . p = r1 holds
f13 . p = 2 * r1 ) & f13 is continuous ) by A56, JGRAPH_2:23;
A58: for p being Point of (TOP-REAL n) holds f13 . p = 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) reconsider X = TOP-REAL n as non empty SubSpace of TOP-REAL n by TSEP_1:2;
consider f14 being Function of X,(TOP-REAL n) such that
A59: ( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being Real st a = b & f13 . a = r holds
f14 . b = r * b ) & f14 is continuous ) by A57, Th2;
reconsider f14 = f14 as continuous Function of (TOP-REAL n),(TOP-REAL n) by A59;
A60: dom f14 = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
A61: for r being Real holds |.r.| * |.r.| = r * r for y being object holds
( y in the carrier of (Tunit_ball n) iff ex x being object st
( x in dom f14 & y = f14 . x ) ) then A70: rng f14 = the carrier of (Tunit_ball n) by FUNCT_1:def 3;
then reconsider f14 = f14 as Function of (TOP-REAL n),(Tunit_ball n) by A60, FUNCT_2:1;
A71: dom f14 = the carrier of (TOP-REAL n) by FUNCT_2:def 1
.= dom (f ") by FUNCT_2:def 1 ;
for x being object st x in dom f14 holds
f14 . x = (f ") . x then f " is continuous by A71, FUNCT_1:2, PRE_TOPC:27;
hence f is being_homeomorphism by A3, A14, A34, A43, A47, TOPS_2:def 5; :: thesis: verum