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

proof

let y be object ; :: thesis: ( y in [#] (TOP-REAL n1) implies ex x being object st [x,y] in f )
assume y in [#] (TOP-REAL n1) ; :: thesis: ex x being object st [x,y] in f
then reconsider py = y as Point of (TOP-REAL n1) ;

per cases ( |.py.| = 0 or |.py.| <> 0 ) ;

suppose A5: |.py.| = 0 ; :: thesis: ex x being object st [x,y] in f

set x = py;
|.(py - (0. (TOP-REAL n1))).| < 1 by A5, RLVECT_1:13;
then py in Ball ((0. (TOP-REAL n)),1) ;
then A6: py in dom f by A3, MFOLD_0:2;
take py ; :: thesis: [py,y] in f
f . py = (1 / (1 - (|.py.| * |.py.|))) * py by A6, A2
.= py by A5, RLVECT_1:def 8 ;
hence [py,y] in f by A6, FUNCT_1:def 2; :: thesis: verum

end;

suppose A7: |.py.| <> 0 ; :: thesis: ex x being object st [x,y] in f

set p2 = |.py.| * |.py.|;
set x = (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py;
reconsider r = 2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) as Real ;
A8: sqrt (1 + (4 * (|.py.| * |.py.|))) >= 0 by SQUARE_1:def 2;
A9: |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| = |.r.| * |.py.| by TOPRNS_1:7
.= r * |.py.| by A8, ABSVALUE:def 1 ;
|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| < 1

proof

(|.py.| * 4) + (1 + (4 * (|.py.| * |.py.|))) > 0 + (1 + (4 * (|.py.| * |.py.|))) by A7, XREAL_1:6;
then sqrt ((1 + (2 * |.py.|)) ^2) > sqrt (1 + (4 * (|.py.| * |.py.|))) by SQUARE_1:27;
then 1 + (2 * |.py.|) > sqrt (1 + (4 * (|.py.| * |.py.|))) by SQUARE_1:22;
then (1 + (2 * |.py.|)) - (sqrt (1 + (4 * (|.py.| * |.py.|)))) > (sqrt (1 + (4 * (|.py.| * |.py.|)))) - (sqrt (1 + (4 * (|.py.| * |.py.|)))) by XREAL_1:9;
then ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * |.py.|)) - (2 * |.py.|) > 0 - (2 * |.py.|) by XREAL_1:9;
then (1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * 1 > - (2 * |.py.|) ;
then (1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) > - (2 * |.py.|) by A8, XCMPLX_1:60;
then (1 - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) > - (2 * |.py.|) ;
then (1 - (1 + (4 * (|.py.| * |.py.|)))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) > - (2 * |.py.|) by SQUARE_1:def 2;
then - ((4 * (|.py.| * |.py.|)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) > - (2 * |.py.|) ;
then ((2 * |.py.|) * (2 * |.py.|)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) < 2 * |.py.| by XREAL_1:24;
then ((2 * |.py.|) * ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) / (2 * |.py.|) < (2 * |.py.|) / (2 * |.py.|) by A7, XREAL_1:74;
then ((2 * |.py.|) * ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) / (2 * |.py.|) < 1 by A7, XCMPLX_1:60;
then ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / ((2 * |.py.|) / (2 * |.py.|)) < 1 by XCMPLX_1:77;
then ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / 1 < 1 by A7, XCMPLX_1:60;
hence |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| < 1 by A9; :: thesis: verum

end;

then |.(((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) - (0. (TOP-REAL n1))).| < 1 by RLVECT_1:13;
then (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py in Ball ((0. (TOP-REAL n1)),1) ;
then A10: (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py in dom f by A3, MFOLD_0:2;
take (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py ; :: thesis: [((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py),y] in f
A11: sqrt (1 + (4 * (|.py.| * |.py.|))) >= 0 by SQUARE_1:def 2;
A12: 1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))) <> 0

proof

assume 1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))) = 0 ; :: thesis: contradiction
then (sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2 = 1 ;
then 1 + (4 * (|.py.| * |.py.|)) = 1 by SQUARE_1:def 2;
hence contradiction by A7; :: thesis: verum

end;

|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| = ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) * (|.py.| * |.py.|) by A9
.= ((2 * 2) / ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) * (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) * (|.py.| * |.py.|) by XCMPLX_1:76
.= (4 / ((1 + (2 * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2))) * (|.py.| * |.py.|)
.= (4 / ((1 + (2 * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + (1 + (4 * (|.py.| * |.py.|))))) * (|.py.| * |.py.|) by SQUARE_1:def 2
.= (4 / (2 * ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * (|.py.| * |.py.|))))) * (|.py.| * |.py.|)
.= ((4 / 2) / ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * (|.py.| * |.py.|)))) * (|.py.| * |.py.|) by XCMPLX_1:78
.= (2 * (|.py.| * |.py.|)) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))) ;
then A13: 1 - (|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).|) = (((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + (- ((2 * (|.py.| * |.py.|)) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) by A11, XCMPLX_1:60
.= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * 1
.= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) / (1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))))) by A12, XCMPLX_1:60
.= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) * (1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) by XCMPLX_1:76
.= (1 - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) * (sqrt (1 + (4 * (|.py.| * |.py.|))))))
.= (1 - (1 + (4 * (|.py.| * |.py.|)))) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) by SQUARE_1:def 2
.= (- (4 * (|.py.| * |.py.|))) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - (1 + (4 * (|.py.| * |.py.|)))) by SQUARE_1:def 2
.= (- (4 * (|.py.| * |.py.|))) / ((- (2 * (|.py.| * |.py.|))) * (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))
.= ((2 * (- (2 * (|.py.| * |.py.|)))) / (- (2 * (|.py.| * |.py.|)))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) by XCMPLX_1:78
.= (2 * ((- (2 * (|.py.| * |.py.|))) / (- (2 * (|.py.| * |.py.|))))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))
.= (2 * 1) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) by A7, XCMPLX_1:60
.= 2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) ;
f . ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) = (1 / (1 - (|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).|))) * ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) by A2, A10
.= (r / r) * py by A13, RLVECT_1:def 7
.= 1 * py by A8, XCMPLX_1:60
.= py by RLVECT_1:def 8 ;
hence [((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py),y] in f by A10, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

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

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
A15: [#] (Tunit_ball n) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;
assume A16: x1 in dom f ; :: thesis: ( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
then reconsider px1 = x1 as Point of (TOP-REAL n1) by A15;
assume A17: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then A18: x2 in the carrier of (Tunit_ball n) ;
reconsider px2 = x2 as Point of (TOP-REAL n1) by A17, A15;
assume A19: f . x1 = f . x2 ; :: thesis: x1 = x2
A20: (1 / (1 - (|.px1.| * |.px1.|))) * px1 = f . x2 by A19, A16, A2
.= (1 / (1 - (|.px2.| * |.px2.|))) * px2 by A17, A2 ;

per cases ( |.px1.| = 0 or |.px1.| <> 0 ) ;

suppose A21: |.px1.| = 0 ; :: thesis: x1 = x2

then (1 / (1 - (|.px2.| * |.px2.|))) * px2 = 0. (TOP-REAL n) by A20, RLVECT_1:10, EUCLID_2:42;

per cases then ( 1 / (1 - (|.px2.| * |.px2.|)) = 0 or px2 = 0. (TOP-REAL n) ) by RLVECT_1:11;

suppose 1 / (1 - (|.px2.| * |.px2.|)) = 0 ; :: thesis: x1 = x2

then 1 - (|.px2.| * |.px2.|) = 0 ;
then sqrt (|.px2.| ^2) = 1 ;
then A22: |.px2.| = 1 by SQUARE_1:22;
px2 in Ball ((0. (TOP-REAL n)),1) by A18, MFOLD_0:2;
then consider p2 being Point of (TOP-REAL n) such that
A23: ( p2 = px2 & |.(p2 - (0. (TOP-REAL n))).| < 1 ) ;
thus x1 = x2 by A22, A23, RLVECT_1:13; :: thesis: verum

end;

suppose px2 = 0. (TOP-REAL n) ; :: thesis: x1 = x2

hence x1 = x2 by A21, EUCLID_2:42; :: thesis: verum

end;

end;

end;

suppose A24: |.px1.| <> 0 ; :: thesis: x1 = x2

then |.px1.| * |.px1.| < 1 * |.px1.| by A16, Th5, XREAL_1:68;
then |.px1.| * |.px1.| < 1 by A16, Th5, XXREAL_0:2;
then - (|.px1.| * |.px1.|) > - 1 by XREAL_1:24;
then A25: (- (|.px1.| * |.px1.|)) + 1 > (- 1) + 1 by XREAL_1:6;
A26: px1 = 1 * px1 by RLVECT_1:def 8
.= ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px1.| * |.px1.|))) * px1 by A25, XCMPLX_1:60
.= (1 - (|.px1.| * |.px1.|)) * ((1 / (1 - (|.px1.| * |.px1.|))) * px1) by RLVECT_1:def 7
.= ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * px2 by A20, RLVECT_1:def 7 ;
A27: px2 <> 0. (TOP-REAL n1)

proof

assume px2 = 0. (TOP-REAL n1) ; :: thesis: contradiction
then px1 = 0. (TOP-REAL n1) by A26, RLVECT_1:10;
hence contradiction by A24, TOPRNS_1:23; :: thesis: verum

end;

then A28: |.px2.| <> 0 by EUCLID_2:42;
px2 in Ball ((0. (TOP-REAL n)),1) by A18, MFOLD_0:2;
then consider p2 being Point of (TOP-REAL n) such that
A29: ( p2 = px2 & |.(p2 - (0. (TOP-REAL n))).| < 1 ) ;
A30: |.px2.| < 1 by A29, RLVECT_1:13;
then |.px2.| * |.px2.| < 1 * |.px2.| by A28, XREAL_1:68;
then |.px2.| * |.px2.| < 1 by A30, XXREAL_0:2;
then - (|.px2.| * |.px2.|) > - 1 by XREAL_1:24;
then A31: (- (|.px2.| * |.px2.|)) + 1 > (- 1) + 1 by XREAL_1:6;
set l = (1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|));
(1 / (1 - (|.px2.| * |.px2.|))) * px2 = ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * px2 by A26, A20, RLVECT_1:def 7;
then ((1 / (1 - (|.px2.| * |.px2.|))) * px2) - (((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * px2) = 0. (TOP-REAL n) by RLVECT_1:5;
then ((1 / (1 - (|.px2.| * |.px2.|))) * px2) + ((- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))) * px2) = 0. (TOP-REAL n) by RLVECT_1:79;
then A32: ((1 / (1 - (|.px2.| * |.px2.|))) + (- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))))) * px2 = 0. (TOP-REAL n) by RLVECT_1:def 6;
A33: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).|

proof

per cases ( |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| = (1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)) or |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| = - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) ) by ABSVALUE:1;

suppose |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| = (1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)) ; :: thesis: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).|

hence ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| ; :: thesis: verum

end;

suppose |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| = - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) ; :: thesis: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).|

hence ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| ; :: thesis: verum

end;

end;

end;

(1 / (1 - (|.px2.| * |.px2.|))) + (- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))) = 0 by A27, A32, RLVECT_1:11;
then 1 / (1 - (|.px2.| * |.px2.|)) = (1 * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) / (1 - (|.px1.| * |.px1.|))
.= 1 / ((1 - (|.px1.| * |.px1.|)) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) by XCMPLX_1:77 ;
then 1 - (|.px2.| * |.px2.|) = (1 - (|.px1.| * |.px1.|)) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) by XCMPLX_1:59;
then ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * (1 - (|.px2.| * |.px2.|)) = (1 - (|.px1.| * |.px1.|)) / (((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) by XCMPLX_1:81
.= (1 - (|.px1.| * |.px1.|)) / 1 by A25, A31, XCMPLX_1:60
.= 1 - ((|.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.px2.|) * |.(((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * px2).|) by A26, TOPRNS_1:7
.= 1 - ((|.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.px2.|) * (|.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.px2.|)) by TOPRNS_1:7
.= 1 - (((|.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).| * |.((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))).|) * |.px2.|) * |.px2.|)
.= 1 - (((((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|) * |.px2.|) by A33 ;
then (1 + ((((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * |.px2.|) * |.px2.|)) * (1 - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) = 0 ;
then 1 - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = 0 by A25, A31;
hence x1 = x2 by A26, RLVECT_1:def 8; :: thesis: verum

end;

end;

end;

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.|)

proof

let p be Point of (TOP-REAL n); :: thesis: f3 . p = 1 - (|.p.| * |.p.|)
thus f3 . p = (f0 . p) - (f2 . p) by A38
.= 1 - (f2 . p) by A35
.= 1 - ((f1 . p) * (f1 . p)) by A37
.= 1 - (|.p.| * (f1 . p)) by A36
.= 1 - (|.p.| * |.p.|) by A36 ; :: thesis: verum

end;

set f4 = f3 | (Tunit_ball n);
for p being Point of (Tunit_ball n) holds (f3 | (Tunit_ball n)) . p <> 0

proof

let p be Point of (Tunit_ball n); :: thesis: (f3 | (Tunit_ball n)) . p <> 0
assume (f3 | (Tunit_ball n)) . p = 0 ; :: thesis: contradiction
then A40: f3 . p = 0 by FUNCT_1:49;
reconsider p1 = p as Point of (TOP-REAL n1) by A4;
A41: 1 - (|.p1.| * |.p1.|) = 0 by A40, A39;

per cases ( |.p1.| = 0 or |.p1.| <> 0 ) ;

suppose |.p1.| = 0 ; :: thesis: contradiction

hence contradiction by A41; :: thesis: verum

end;

suppose |.p1.| <> 0 ; :: thesis: contradiction

then |.p1.| * |.p1.| < 1 * |.p1.| by Th5, XREAL_1:68;
hence contradiction by A41, Th5; :: thesis: verum

end;

end;

end;

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

proof

let x be object ; :: thesis: ( x in dom f implies f . x = f6 . x )
assume A45: x in dom f ; :: thesis: f . x = f6 . x
then reconsider p1 = x as Point of (Tunit_ball n) ;
reconsider p = x as Point of (TOP-REAL n) by A45, A4;
(f3 | (Tunit_ball n)) . p = f3 . p by A45, FUNCT_1:49
.= 1 - (|.p.| * |.p.|) by A39 ;
then f5 . p1 = 1 / (1 - (|.p.| * |.p.|)) by A42;
then f6 . p1 = (1 / (1 - (|.p.| * |.p.|))) * p by A43;
hence f . x = f6 . x by A2; :: thesis: verum

end;

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.|)

proof

let p be Point of (TOP-REAL n); :: thesis: f9 . p = 1 + ((4 * |.p.|) * |.p.|)
thus f9 . p = (f0 . p) + (f8 . p) by A49
.= 1 + (f8 . p) by A35
.= 1 + (4 * (f2 . p)) by A48
.= 1 + (4 * ((f1 . p) * (f1 . p))) by A37
.= 1 + (4 * ((f1 . p) * |.p.|)) by A36
.= 1 + (4 * (|.p.| * |.p.|)) by A36
.= 1 + ((4 * |.p.|) * |.p.|) ; :: thesis: verum

end;

A51: for p being Point of (TOP-REAL n) ex r being Real st
( f9 . p = r & r >= 0 )

proof

let p be Point of (TOP-REAL n); :: thesis: ex r being Real st
( f9 . p = r & r >= 0 )
set r = 1 + ((4 * |.p.|) * |.p.|);
take 1 + ((4 * |.p.|) * |.p.|) ; :: thesis: ( f9 . p = 1 + ((4 * |.p.|) * |.p.|) & 1 + ((4 * |.p.|) * |.p.|) >= 0 )
thus ( f9 . p = 1 + ((4 * |.p.|) * |.p.|) & 1 + ((4 * |.p.|) * |.p.|) >= 0 ) by A50; :: thesis: verum

end;

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

proof

let p be Point of (TOP-REAL n); :: thesis: f11 . p <> 0
A54: f11 . p = (f0 . p) + (f10 . p) by A53
.= 1 + (f10 . p) by A35
.= 1 + (sqrt (f9 . p)) by A52 ;
consider r being Real such that
A55: ( r = f9 . p & r >= 0 ) by A51;
sqrt (f9 . p) >= 0 by A55, SQUARE_1:def 2;
hence f11 . p <> 0 by A54; :: thesis: verum

end;

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.|))))

proof

let p be Point of (TOP-REAL n); :: thesis: f13 . p = 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))
thus f13 . p = 2 * (f12 . p) by A57
.= 2 * (1 / (f11 . p)) by A56
.= 2 / ((f0 . p) + (f10 . p)) by A53
.= 2 / ((f0 . p) + (sqrt (f9 . p))) by A52
.= 2 / (1 + (sqrt (f9 . p))) by A35
.= 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) by A50 ; :: thesis: verum

end;

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

proof

let r be Real; :: thesis: |.r.| * |.r.| = r * r

per cases ( |.r.| = r or |.r.| = - r ) by ABSVALUE:1;

suppose |.r.| = r ; :: thesis: |.r.| * |.r.| = r * r

hence |.r.| * |.r.| = r * r ; :: thesis: verum

end;

suppose |.r.| = - r ; :: thesis: |.r.| * |.r.| = r * r

hence |.r.| * |.r.| = r * r ; :: thesis: verum

end;

end;

end;

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 ) )

proof

let y be object ; :: thesis: ( y in the carrier of (Tunit_ball n) iff ex x being object st
( x in dom f14 & y = f14 . x ) )

hereby :: thesis: ( ex x being object st
( x in dom f14 & y = f14 . x ) implies y in the carrier of (Tunit_ball n) )

assume A62: y in the carrier of (Tunit_ball n) ; :: thesis: ex x being object st
( x in dom f14 & f14 . x = y )
[#] (Tunit_ball n) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;
then reconsider q = y as Point of (TOP-REAL n1) by A62;
|.q.| < 1 by A62, Th5;
then |.q.| * |.q.| <= 1 * |.q.| by XREAL_1:64;
then |.q.| * |.q.| < 1 by A62, Th5, XXREAL_0:2;
then A63: 0 < 1 - (|.q.| * |.q.|) by XREAL_1:50;
set p = (1 / (1 - (|.q.| * |.q.|))) * q;
|.((1 / (1 - (|.q.| * |.q.|))) * q).| = |.(1 / (1 - (|.q.| * |.q.|))).| * |.q.| by TOPRNS_1:7;
then |.((1 / (1 - (|.q.| * |.q.|))) * q).| * |.((1 / (1 - (|.q.| * |.q.|))) * q).| = ((|.(1 / (1 - (|.q.| * |.q.|))).| * |.(1 / (1 - (|.q.| * |.q.|))).|) * |.q.|) * |.q.|
.= (((1 / (1 - (|.q.| * |.q.|))) * (1 / (1 - (|.q.| * |.q.|)))) * |.q.|) * |.q.| by A61
.= (((1 * 1) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|)))) * |.q.|) * |.q.| by XCMPLX_1:76
.= (|.q.| * |.q.|) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|))) ;
then A64: 1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) = (((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|))) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|)))) + (((4 * |.q.|) * |.q.|) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|)))) by A63, XCMPLX_1:60
.= ((1 + (|.q.| * |.q.|)) * (1 + (|.q.| * |.q.|))) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|)))
.= ((1 + (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) ^2 by XCMPLX_1:76 ;
sqrt (1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|)) = (1 + (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|)) by A63, A64, SQUARE_1:22;
then A65: 1 + (sqrt (1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|))) = ((1 - (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) + ((1 + (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) by A63, XCMPLX_1:60
.= 2 / (1 - (|.q.| * |.q.|)) ;
reconsider x = (1 / (1 - (|.q.| * |.q.|))) * q as object ;
take x = x; :: thesis: ( x in dom f14 & f14 . x = y )
thus x in dom f14 by A60; :: thesis: f14 . x = y
thus f14 . x = (f13 . ((1 / (1 - (|.q.| * |.q.|))) * q)) * ((1 / (1 - (|.q.| * |.q.|))) * q) by A59
.= (2 / (2 / (1 - (|.q.| * |.q.|)))) * ((1 / (1 - (|.q.| * |.q.|))) * q) by A65, A58
.= (1 - (|.q.| * |.q.|)) * ((1 / (1 - (|.q.| * |.q.|))) * q) by XCMPLX_1:52
.= ((1 - (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) * q by RLVECT_1:def 7
.= 1 * q by A63, XCMPLX_1:60
.= y by RLVECT_1:def 8 ; :: thesis: verum

end;

given x being object such that A66: ( x in dom f14 & y = f14 . x ) ; :: thesis: y in the carrier of (Tunit_ball n)
reconsider p = x as Point of (TOP-REAL n1) by A66;
y in rng f14 by A66, FUNCT_1:3;
then reconsider q = y as Point of (TOP-REAL n1) ;
y = (f13 . p) * p by A59, A66
.= (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) * p by A58 ;
then |.q.| = |.(2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))).| * |.p.| by TOPRNS_1:7;
then A67: |.q.| * |.q.| = ((|.(2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))).| * |.(2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))).|) * |.p.|) * |.p.|
.= (((2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) * (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| by A61 ;
|.q.| * |.q.| < 1

proof

assume |.q.| * |.q.| >= 1 ; :: thesis: contradiction
then A68: (((2 * 2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| >= 1 by A67, XCMPLX_1:76;
0 <= sqrt (1 + ((4 * |.p.|) * |.p.|)) by SQUARE_1:def 2;
then (((4 / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)) * |.p.|) * |.p.|) * ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) >= 1 * ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) by A68, XREAL_1:64;
then (((((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)) * 4) * |.p.|) * |.p.| >= (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2 ;
then ((1 * 4) * |.p.|) * |.p.| >= (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2 by XCMPLX_1:60;
then (4 * |.p.|) * |.p.| >= (1 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + ((sqrt (1 + ((4 * |.p.|) * |.p.|))) ^2) ;
then (4 * |.p.|) * |.p.| >= (1 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + (1 + ((4 * |.p.|) * |.p.|)) by SQUARE_1:def 2;
then ((4 * |.p.|) * |.p.|) - ((4 * |.p.|) * |.p.|) >= ((2 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + ((4 * |.p.|) * |.p.|)) - ((4 * |.p.|) * |.p.|) by XREAL_1:9;
then 0 / 2 > (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|)))) / 2 ;
hence contradiction by SQUARE_1:def 2; :: thesis: verum

end;

then |.q.| ^2 < 1 ;
then A69: |.q.| < 1 by SQUARE_1:52;
|.(q + (- (0. (TOP-REAL n1)))).| <= |.q.| + |.(- (0. (TOP-REAL n1))).| by EUCLID_2:52;
then |.(q + (- (0. (TOP-REAL n1)))).| <= |.q.| + |.(0. (TOP-REAL n1)).| by JGRAPH_5:10;
then |.(q + (- (0. (TOP-REAL n1)))).| <= |.q.| + 0 by EUCLID_2:39;
then |.(q - (0. (TOP-REAL n1))).| < 1 by A69, XXREAL_0:2;
then q in Ball ((0. (TOP-REAL n1)),1) ;
then y in [#] (Tball ((0. (TOP-REAL n)),1)) by PRE_TOPC:def 5;
hence y in the carrier of (Tunit_ball n) ; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in dom f14 implies f14 . x = (f ") . x )
assume A72: x in dom f14 ; :: thesis: f14 . x = (f ") . x
reconsider g = f as Function ;
f is onto by A14, FUNCT_2:def 3;
then A73: f " = g " by A34, TOPS_2:def 4;
A74: f14 . x in rng f14 by A72, FUNCT_1:3;
then A75: f14 . x in dom f by A70, FUNCT_2:def 1;
reconsider p = x as Point of (TOP-REAL n1) by A72;
A76: f14 . p = (f13 . p) * p by A59
.= (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) * p by A58 ;
reconsider y = f14 . x as Point of (Tunit_ball n) by A74;
reconsider q = y as Point of (TOP-REAL n1) by A4;
A77: 0 <= sqrt (1 + ((4 * |.p.|) * |.p.|)) by SQUARE_1:def 2;
|.q.| = |.(2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))).| * |.p.| by A76, TOPRNS_1:7;
then |.q.| * |.q.| = ((|.(2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))).| * |.(2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))).|) * |.p.|) * |.p.|
.= (((2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) * (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| by A61
.= (((2 * 2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| by XCMPLX_1:76
.= ((4 * |.p.|) * |.p.|) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) ;
then A78: 1 - (|.q.| * |.q.|) = (((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)) - (((4 * |.p.|) * |.p.|) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)) by A77, XCMPLX_1:60
.= (((1 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + ((sqrt (1 + ((4 * |.p.|) * |.p.|))) ^2)) - ((4 * |.p.|) * |.p.|)) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)
.= (((1 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + (1 + ((4 * |.p.|) * |.p.|))) - ((4 * |.p.|) * |.p.|)) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) by SQUARE_1:def 2
.= (2 * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))
.= 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) by A77, XCMPLX_1:91 ;
f . (f14 . x) = (1 / (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * q by A2, A78
.= ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) / 2) * q by XCMPLX_1:57
.= (((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) / 2) * (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * p by A76, RLVECT_1:def 7
.= ((2 * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) / (2 * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * p by XCMPLX_1:76
.= 1 * p by A77, XCMPLX_1:60
.= p by RLVECT_1:def 8 ;
then [(f14 . x),x] in f by A75, FUNCT_1:def 2;
then [x,(f14 . x)] in g ~ by RELAT_1:def 7;
then [x,(f14 . x)] in g " by A34, FUNCT_1:def 5;
hence f14 . x = (f ") . x by A73, FUNCT_1:1; :: thesis: verum

end;

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