let n be Nat; :: thesis: for p being Point of (TOP-REAL n)

for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds

stereographic_projection (S,p) is being_homeomorphism

let p be Point of (TOP-REAL n); :: thesis: for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds

stereographic_projection (S,p) is being_homeomorphism

let S be SubSpace of TOP-REAL n; :: thesis: ( [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) implies stereographic_projection (S,p) is being_homeomorphism )

assume A1: [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} ; :: thesis: ( not p in Sphere ((0. (TOP-REAL n)),1) or stereographic_projection (S,p) is being_homeomorphism )

assume A2: p in Sphere ((0. (TOP-REAL n)),1) ; :: thesis: stereographic_projection (S,p) is being_homeomorphism

set f = stereographic_projection (S,p);

set T = TPlane (p,(0. (TOP-REAL n)));

A3: dom (stereographic_projection (S,p)) = [#] S by FUNCT_2:def 1;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider p1 = p as Point of (TOP-REAL n1) ;

|.(p1 - (0. (TOP-REAL n1))).| = 1 by A2, TOPREAL9:9;

then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;

then |.(p1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;

then A4: |.p.| = 1 by RLVECT_1:4;

then |(p,p)| = 1 ^2 by EUCLID_2:4;

then A5: |(p,p)| = 1 * 1 by SQUARE_1:def 1;

defpred S_{1}[ object , object ] means for q being Point of (TOP-REAL n) st q = $1 & q in TPlane (p,(0. (TOP-REAL n))) holds

$2 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p));

A6: for x being object st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds

ex y being object st

( y in [#] S & S_{1}[x,y] )

A18: for x being object st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds

S_{1}[x,g1 . x]
from FUNCT_2:sch 1(A6);

reconsider g = g1 as Function of (TPlane (p,(0. (TOP-REAL n)))),S ;

reconsider f1 = stereographic_projection (S,p) as Function of ([#] S),([#] (TPlane (p,(0. (TOP-REAL n))))) ;

|.(0. (TOP-REAL n)).| <> |.p.| by A4, EUCLID_2:39;

then 0. (TOP-REAL n) <> (1 + 1) * p by RLVECT_1:11;

then 0. (TOP-REAL n) <> (1 * p) + (1 * p) by RLVECT_1:def 6;

then 0. (TOP-REAL n) <> (1 * p) + p by RLVECT_1:def 8;

then 0. (TOP-REAL n) <> p + p by RLVECT_1:def 8;

then p + (- p) <> p + p by RLVECT_1:5;

then A19: not - p in {p} by TARSKI:def 1;

|.(- p).| = 1 by A4, EUCLID:71;

then |.((- p) + (0. (TOP-REAL n))).| = 1 by RLVECT_1:4;

then |.((- p) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by RLVECT_1:10;

then |.((- p) - (0. (TOP-REAL n))).| = 1 by RLVECT_1:16;

then A20: - p in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;

then A21: [#] S <> {} by A1, A19, XBOOLE_0:def 5;

A22: for y, x being object holds

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) )

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) iff ex x being object st

( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) )

A62: stereographic_projection (S,p) is one-to-one

f2 is onto by A61, FUNCT_2:def 3;

then A122: f1 " = f1 " by A62, TOPS_2:def 4;

g1 = f1 " by A61, A62, A22, A21, FUNCT_2:28;

hence stereographic_projection (S,p) is being_homeomorphism by A3, A61, A62, A65, A96, A122, TOPS_2:def 5; :: thesis: verum

for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds

stereographic_projection (S,p) is being_homeomorphism

let p be Point of (TOP-REAL n); :: thesis: for S being SubSpace of TOP-REAL n st [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) holds

stereographic_projection (S,p) is being_homeomorphism

let S be SubSpace of TOP-REAL n; :: thesis: ( [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} & p in Sphere ((0. (TOP-REAL n)),1) implies stereographic_projection (S,p) is being_homeomorphism )

assume A1: [#] S = (Sphere ((0. (TOP-REAL n)),1)) \ {p} ; :: thesis: ( not p in Sphere ((0. (TOP-REAL n)),1) or stereographic_projection (S,p) is being_homeomorphism )

assume A2: p in Sphere ((0. (TOP-REAL n)),1) ; :: thesis: stereographic_projection (S,p) is being_homeomorphism

set f = stereographic_projection (S,p);

set T = TPlane (p,(0. (TOP-REAL n)));

A3: dom (stereographic_projection (S,p)) = [#] S by FUNCT_2:def 1;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider p1 = p as Point of (TOP-REAL n1) ;

|.(p1 - (0. (TOP-REAL n1))).| = 1 by A2, TOPREAL9:9;

then |.(p1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;

then |.(p1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;

then A4: |.p.| = 1 by RLVECT_1:4;

then |(p,p)| = 1 ^2 by EUCLID_2:4;

then A5: |(p,p)| = 1 * 1 by SQUARE_1:def 1;

defpred S

$2 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p));

A6: for x being object st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds

ex y being object st

( y in [#] S & S

proof

consider g1 being Function of ([#] (TPlane (p,(0. (TOP-REAL n))))),([#] S) such that
let x be object ; :: thesis: ( x in [#] (TPlane (p,(0. (TOP-REAL n)))) implies ex y being object st

( y in [#] S & S_{1}[x,y] ) )

assume A7: x in [#] (TPlane (p,(0. (TOP-REAL n)))) ; :: thesis: ex y being object st

( y in [#] S & S_{1}[x,y] )

[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider q = x as Point of (TOP-REAL n) by A7;

set y = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p));

take (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) ; :: thesis: ( (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S & S_{1}[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))] )

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider p1 = p as Point of (TOP-REAL n1) ;

q in Plane (p,(0. (TOP-REAL n))) by A7, PRE_TOPC:def 5;

then consider x1 being Point of (TOP-REAL n) such that

A8: ( x1 = q & |(p,(x1 - (0. (TOP-REAL n))))| = 0 ) ;

|(p,(q + ((- 1) * (0. (TOP-REAL n)))))| = 0 by A8, RLVECT_1:16;

then |(p,(q + (0. (TOP-REAL n))))| = 0 by RLVECT_1:10;

then A9: |(p,q)| = 0 by RLVECT_1:4;

A10: |(q,q)| >= 0 by EUCLID_2:35;

A11: not (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in {p}

A14: |(q,((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * |(q,q)|) + ((|(q,q)| - 1) * |(p,q)|) by EUCLID_2:25

.= 2 * |(q,q)| by A9 ;

A15: |(p,((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * |(q,p)|) + ((|(q,q)| - 1) * |(p,p)|) by EUCLID_2:25

.= |(q,q)| - 1 by A5, A9 ;

A16: |(((2 * q) + ((|(q,q)| - 1) * p)),((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * (2 * |(q,q)|)) + ((|(q,q)| - 1) * |(p,((2 * q) + ((|(q,q)| - 1) * p)))|) by A14, EUCLID_2:25

.= (|(q,q)| + 1) * (|(q,q)| + 1) by A15 ;

A17: |(((2 * q) + ((|(q,q)| - 1) * p)),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),((2 * q) + ((|(q,q)| - 1) * p)))| by EUCLID_2:20;

|(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| by EUCLID_2:19

.= ((1 / (|(q,q)| + 1)) * ((1 / (|(q,q)| + 1)) * (|(q,q)| + 1))) * (|(q,q)| + 1) by A16, A17

.= ((1 / (|(q,q)| + 1)) * ((|(q,q)| + 1) / (|(q,q)| + 1))) * (|(q,q)| + 1) by XCMPLX_1:99

.= ((1 / (|(q,q)| + 1)) * 1) * (|(q,q)| + 1) by A10, XCMPLX_1:60

.= (|(q,q)| + 1) / (|(q,q)| + 1) by XCMPLX_1:99

.= 1 by A10, XCMPLX_1:60 ;

then |.((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))).| = 1 by EUCLID_2:5, SQUARE_1:18;

then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + (0. (TOP-REAL n))).| = 1 by RLVECT_1:4;

then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by RLVECT_1:10;

then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) - (0. (TOP-REAL n))).| = 1 by RLVECT_1:16;

then y1 in Sphere ((0. (TOP-REAL n)),1) by TOPREAL9:9;

hence (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S by A1, A11, XBOOLE_0:def 5; :: thesis: S_{1}[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))]

thus S_{1}[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))]
; :: thesis: verum

end;( y in [#] S & S

assume A7: x in [#] (TPlane (p,(0. (TOP-REAL n)))) ; :: thesis: ex y being object st

( y in [#] S & S

[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider q = x as Point of (TOP-REAL n) by A7;

set y = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p));

take (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) ; :: thesis: ( (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S & S

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider p1 = p as Point of (TOP-REAL n1) ;

q in Plane (p,(0. (TOP-REAL n))) by A7, PRE_TOPC:def 5;

then consider x1 being Point of (TOP-REAL n) such that

A8: ( x1 = q & |(p,(x1 - (0. (TOP-REAL n))))| = 0 ) ;

|(p,(q + ((- 1) * (0. (TOP-REAL n)))))| = 0 by A8, RLVECT_1:16;

then |(p,(q + (0. (TOP-REAL n))))| = 0 by RLVECT_1:10;

then A9: |(p,q)| = 0 by RLVECT_1:4;

A10: |(q,q)| >= 0 by EUCLID_2:35;

A11: not (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in {p}

proof

reconsider y1 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) as Point of (TOP-REAL n1) ;
assume A12:
(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in {p}
; :: thesis: contradiction

A13: |(((2 * q) + ((|(q,q)| - 1) * p)),p)| = (2 * |(q,p)|) + ((|(q,q)| - 1) * |(p,p)|) by EUCLID_2:25

.= (|(q,q)| - 1) * |(p,p)| by A9 ;

|(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))),p)| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),p)| by EUCLID_2:19

.= ((1 / (|(q,q)| + 1)) * (|(q,q)| - 1)) * |(p,p)| by A13 ;

then (|(q,q)| + 1) * 1 = (|(q,q)| + 1) * ((1 / (|(q,q)| + 1)) * (|(q,q)| - 1)) by A5, A12, TARSKI:def 1

.= ((|(q,q)| + 1) * (1 / (|(q,q)| + 1))) * (|(q,q)| - 1)

.= ((|(q,q)| + 1) / (|(q,q)| + 1)) * (|(q,q)| - 1) by XCMPLX_1:99

.= 1 * (|(q,q)| - 1) by A10, XCMPLX_1:60 ;

hence contradiction ; :: thesis: verum

end;A13: |(((2 * q) + ((|(q,q)| - 1) * p)),p)| = (2 * |(q,p)|) + ((|(q,q)| - 1) * |(p,p)|) by EUCLID_2:25

.= (|(q,q)| - 1) * |(p,p)| by A9 ;

|(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))),p)| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),p)| by EUCLID_2:19

.= ((1 / (|(q,q)| + 1)) * (|(q,q)| - 1)) * |(p,p)| by A13 ;

then (|(q,q)| + 1) * 1 = (|(q,q)| + 1) * ((1 / (|(q,q)| + 1)) * (|(q,q)| - 1)) by A5, A12, TARSKI:def 1

.= ((|(q,q)| + 1) * (1 / (|(q,q)| + 1))) * (|(q,q)| - 1)

.= ((|(q,q)| + 1) / (|(q,q)| + 1)) * (|(q,q)| - 1) by XCMPLX_1:99

.= 1 * (|(q,q)| - 1) by A10, XCMPLX_1:60 ;

hence contradiction ; :: thesis: verum

A14: |(q,((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * |(q,q)|) + ((|(q,q)| - 1) * |(p,q)|) by EUCLID_2:25

.= 2 * |(q,q)| by A9 ;

A15: |(p,((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * |(q,p)|) + ((|(q,q)| - 1) * |(p,p)|) by EUCLID_2:25

.= |(q,q)| - 1 by A5, A9 ;

A16: |(((2 * q) + ((|(q,q)| - 1) * p)),((2 * q) + ((|(q,q)| - 1) * p)))| = (2 * (2 * |(q,q)|)) + ((|(q,q)| - 1) * |(p,((2 * q) + ((|(q,q)| - 1) * p)))|) by A14, EUCLID_2:25

.= (|(q,q)| + 1) * (|(q,q)| + 1) by A15 ;

A17: |(((2 * q) + ((|(q,q)| - 1) * p)),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),((2 * q) + ((|(q,q)| - 1) * p)))| by EUCLID_2:20;

|(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| = (1 / (|(q,q)| + 1)) * |(((2 * q) + ((|(q,q)| - 1) * p)),((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))))| by EUCLID_2:19

.= ((1 / (|(q,q)| + 1)) * ((1 / (|(q,q)| + 1)) * (|(q,q)| + 1))) * (|(q,q)| + 1) by A16, A17

.= ((1 / (|(q,q)| + 1)) * ((|(q,q)| + 1) / (|(q,q)| + 1))) * (|(q,q)| + 1) by XCMPLX_1:99

.= ((1 / (|(q,q)| + 1)) * 1) * (|(q,q)| + 1) by A10, XCMPLX_1:60

.= (|(q,q)| + 1) / (|(q,q)| + 1) by XCMPLX_1:99

.= 1 by A10, XCMPLX_1:60 ;

then |.((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))).| = 1 by EUCLID_2:5, SQUARE_1:18;

then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + (0. (TOP-REAL n))).| = 1 by RLVECT_1:4;

then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by RLVECT_1:10;

then |.(((1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))) - (0. (TOP-REAL n))).| = 1 by RLVECT_1:16;

then y1 in Sphere ((0. (TOP-REAL n)),1) by TOPREAL9:9;

hence (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) in [#] S by A1, A11, XBOOLE_0:def 5; :: thesis: S

thus S

A18: for x being object st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds

S

reconsider g = g1 as Function of (TPlane (p,(0. (TOP-REAL n)))),S ;

reconsider f1 = stereographic_projection (S,p) as Function of ([#] S),([#] (TPlane (p,(0. (TOP-REAL n))))) ;

|.(0. (TOP-REAL n)).| <> |.p.| by A4, EUCLID_2:39;

then 0. (TOP-REAL n) <> (1 + 1) * p by RLVECT_1:11;

then 0. (TOP-REAL n) <> (1 * p) + (1 * p) by RLVECT_1:def 6;

then 0. (TOP-REAL n) <> (1 * p) + p by RLVECT_1:def 8;

then 0. (TOP-REAL n) <> p + p by RLVECT_1:def 8;

then p + (- p) <> p + p by RLVECT_1:5;

then A19: not - p in {p} by TARSKI:def 1;

|.(- p).| = 1 by A4, EUCLID:71;

then |.((- p) + (0. (TOP-REAL n))).| = 1 by RLVECT_1:4;

then |.((- p) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by RLVECT_1:10;

then |.((- p) - (0. (TOP-REAL n))).| = 1 by RLVECT_1:16;

then A20: - p in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;

then A21: [#] S <> {} by A1, A19, XBOOLE_0:def 5;

A22: for y, x being object holds

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) )

proof

for y being object holds
let y, x be object ; :: thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x iff ( x in [#] S & f1 . x = y ) )

assume A38: f1 . x = y ; :: thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x )

hence y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A37, FUNCT_2:5; :: thesis: g1 . y = x

[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qx = x as Point of (TOP-REAL n) by A37;

qx in S by A37;

then A40: y = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by A38, A2, Def5;

then reconsider qy = y as Point of (TOP-REAL n) ;

A41: qy in TPlane (p,(0. (TOP-REAL n))) by A38, A37, FUNCT_2:5;

A42: g1 . qy = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A41, A18;

reconsider qx1 = qx as Point of (TOP-REAL n1) ;

qx1 in Sphere ((0. (TOP-REAL n)),1) by A37, A1, XBOOLE_0:def 5;

then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;

then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;

then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;

then |.qx.| = 1 by RLVECT_1:4;

then |(qx,qx)| = 1 ^2 by EUCLID_2:4;

then A43: |(qx,qx)| = 1 * 1 by SQUARE_1:def 1;

A44: |((|(qx,p)| * p),(qx - (|(qx,p)| * p)))| = |((|(qx,p)| * p),qx)| - |((|(qx,p)| * p),(|(qx,p)| * p))| by EUCLID_2:27

.= (|(qx,p)| * |(qx,p)|) - |((|(qx,p)| * p),(|(qx,p)| * p))| by EUCLID_2:19

.= (|(qx,p)| * |(qx,p)|) - (|(qx,p)| * |(p,(|(qx,p)| * p))|) by EUCLID_2:19

.= (|(qx,p)| * |(qx,p)|) - (|(qx,p)| * (|(qx,p)| * |(p,p)|)) by EUCLID_2:20

.= 0 by A5 ;

A45: |(qx,(qx - (|(qx,p)| * p)))| = |(qx,qx)| - |(qx,(|(qx,p)| * p))| by EUCLID_2:24

.= 1 - (|(qx,p)| * |(qx,p)|) by A43, EUCLID_2:20 ;

A46: |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))| = |(qx,(qx - (|(qx,p)| * p)))| - |((|(qx,p)| * p),(qx - (|(qx,p)| * p)))| by EUCLID_2:24

.= (1 - (|(qx,p)| * |(qx,p)|)) + 0 by A45, A44 ;

|(qx,p)| <> 1

then A52: (1 - |(qx,p)|) * (1 - |(qx,p)|) <> 0 ;

A53: |(qy,qy)| = (1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),qy)| by A40, EUCLID_2:19

.= (1 / (1 - |(qx,p)|)) * ((1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))|) by A40, EUCLID_2:19

.= ((1 / (1 - |(qx,p)|)) * (1 / (1 - |(qx,p)|))) * (1 - (|(qx,p)| * |(qx,p)|)) by A46

.= (1 / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) * (1 - (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:102

.= (1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:99 ;

A54: |(qy,qy)| + 1 = ((1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) + (((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) by A53, A52, XCMPLX_1:60

.= ((1 - (|(qx,p)| * |(qx,p)|)) + ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:62

.= (2 * (1 - |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))

.= 2 * ((1 - |(qx,p)|) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) by XCMPLX_1:74

.= 2 * (((1 - |(qx,p)|) / (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:78

.= 2 * (1 / (1 - |(qx,p)|)) by A51, XCMPLX_1:60

.= (2 * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ;

A55: |(qy,qy)| - 1 = ((1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) - (((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) by A53, A52, XCMPLX_1:60

.= ((1 - (|(qx,p)| * |(qx,p)|)) - ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:120

.= ((2 * |(qx,p)|) * (1 - |(qx,p)|)) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))

.= (2 * |(qx,p)|) * ((1 - |(qx,p)|) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) by XCMPLX_1:74

.= (2 * |(qx,p)|) * (((1 - |(qx,p)|) / (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:78

.= (2 * |(qx,p)|) * (1 / (1 - |(qx,p)|)) by A51, XCMPLX_1:60

.= ((2 * |(qx,p)|) * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ;

A56: 1 / (|(qy,qy)| + 1) = (1 - |(qx,p)|) / 2 by A54, XCMPLX_1:57;

A57: (|(qy,qy)| - 1) / (|(qy,qy)| + 1) = (2 * |(qx,p)|) / ((1 - |(qx,p)|) * (2 / (1 - |(qx,p)|))) by A54, A55, XCMPLX_1:78

.= (2 * |(qx,p)|) / ((2 * (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:74

.= (2 * |(qx,p)|) / (2 * ((1 - |(qx,p)|) / (1 - |(qx,p)|))) by XCMPLX_1:74

.= (2 * |(qx,p)|) / (2 * 1) by A51, XCMPLX_1:60

.= |(qx,p)| ;

A58: (1 - |(qx,p)|) * qy = ((1 - |(qx,p)|) * (1 / (1 - |(qx,p)|))) * (qx - (|(qx,p)| * p)) by A40, RLVECT_1:def 7

.= (((1 - |(qx,p)|) * 1) / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by XCMPLX_1:74

.= 1 * (qx - (|(qx,p)| * p)) by A51, XCMPLX_1:60

.= qx - (|(qx,p)| * p) by RLVECT_1:def 8 ;

thus g1 . y = ((1 / (|(qy,qy)| + 1)) * (2 * qy)) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by A42, RLVECT_1:def 5

.= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 7

.= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + (((1 / (|(qy,qy)| + 1)) * (|(qy,qy)| - 1)) * p) by RLVECT_1:def 7

.= ((1 - |(qx,p)|) * qy) + (((1 * (|(qy,qy)| - 1)) / (|(qy,qy)| + 1)) * p) by A56, XCMPLX_1:74

.= qx - ((|(qx,p)| * p) - (|(qx,p)| * p)) by A57, A58, RLVECT_1:29

.= qx - (0. (TOP-REAL n)) by RLVECT_1:5

.= qx + ((- 1) * (0. (TOP-REAL n))) by RLVECT_1:16

.= qx + (0. (TOP-REAL n)) by RLVECT_1:10

.= x by RLVECT_1:4 ; :: thesis: verum

end;hereby :: thesis: ( x in [#] S & f1 . x = y implies ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x ) )

assume A37:
x in [#] S
; :: thesis: ( not f1 . x = y or ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x ) )assume A23:
y in [#] (TPlane (p,(0. (TOP-REAL n))))
; :: thesis: ( g1 . y = x implies ( x in [#] S & f1 . x = y ) )

assume A24: g1 . y = x ; :: thesis: ( x in [#] S & f1 . x = y )

hence A25: x in [#] S by A23, A21, FUNCT_2:5; :: thesis: f1 . x = y

[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qx = x as Point of (TOP-REAL n) by A25;

[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qy = y as Point of (TOP-REAL n) by A23;

qy in TPlane (p,(0. (TOP-REAL n))) by A23;

then A26: qx = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A18, A24;

qx in S by A24, A23, A21, FUNCT_2:5;

then A27: (stereographic_projection (S,p)) . qx = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by A2, Def5;

qy in Plane (p,(0. (TOP-REAL n))) by A23, PRE_TOPC:def 5;

then consider y1 being Point of (TOP-REAL n) such that

A28: ( y1 = qy & |(p,(y1 - (0. (TOP-REAL n))))| = 0 ) ;

|(p,(qy + ((- 1) * (0. (TOP-REAL n)))))| = 0 by A28, RLVECT_1:16;

then |(p,(qy + (0. (TOP-REAL n))))| = 0 by RLVECT_1:10;

then A29: |(p,qy)| = 0 by RLVECT_1:4;

A30: |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| = (2 * |(qy,p)|) + ((|(qy,qy)| - 1) * |(p,p)|) by EUCLID_2:25

.= |(qy,qy)| - 1 by A5, A29 ;

A31: |(qx,p)| = (1 / (|(qy,qy)| + 1)) * |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| by A26, EUCLID_2:19

.= ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) * 1 by A30, XCMPLX_1:75 ;

A32: |(qy,qy)| >= 0 by EUCLID_2:35;

A33: 1 - |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) - ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) by A31, A32, XCMPLX_1:60

.= ((|(qy,qy)| + 1) - (|(qy,qy)| - 1)) / (|(qy,qy)| + 1) by XCMPLX_1:120

.= 2 / (|(qy,qy)| + 1) ;

A34: 1 / (1 - |(qx,p)|) = (|(qy,qy)| + 1) / 2 by A33, XCMPLX_1:57;

A35: ((|(qy,qy)| + 1) / 2) * qx = (((|(qy,qy)| + 1) / 2) * (1 / (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A26, RLVECT_1:def 7

.= (((|(qy,qy)| + 1) * 1) / (2 * (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by XCMPLX_1:76

.= (((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * (1 / 2)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by XCMPLX_1:76

.= (1 * (1 / 2)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A32, XCMPLX_1:60

.= ((1 / 2) * (2 * qy)) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 5

.= (((1 / 2) * 2) * qy) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 7

.= (1 * qy) + (((1 / 2) * (|(qy,qy)| - 1)) * p) by RLVECT_1:def 7

.= qy + (((|(qy,qy)| - 1) / 2) * p) by RLVECT_1:def 8 ;

A36: ((|(qy,qy)| + 1) / 2) * |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) / 2) by A31, XCMPLX_1:85

.= 1 * ((|(qy,qy)| - 1) / 2) by A32, XCMPLX_1:60

.= (|(qy,qy)| - 1) / 2 ;

thus f1 . x = (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| + 1) / 2) * (|(qx,p)| * p)) by A27, A34, RLVECT_1:34

.= (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| - 1) / 2) * p) by A36, RLVECT_1:def 7

.= y by A35, RLVECT_4:1 ; :: thesis: verum

end;assume A24: g1 . y = x ; :: thesis: ( x in [#] S & f1 . x = y )

hence A25: x in [#] S by A23, A21, FUNCT_2:5; :: thesis: f1 . x = y

[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qx = x as Point of (TOP-REAL n) by A25;

[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qy = y as Point of (TOP-REAL n) by A23;

qy in TPlane (p,(0. (TOP-REAL n))) by A23;

then A26: qx = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A18, A24;

qx in S by A24, A23, A21, FUNCT_2:5;

then A27: (stereographic_projection (S,p)) . qx = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by A2, Def5;

qy in Plane (p,(0. (TOP-REAL n))) by A23, PRE_TOPC:def 5;

then consider y1 being Point of (TOP-REAL n) such that

A28: ( y1 = qy & |(p,(y1 - (0. (TOP-REAL n))))| = 0 ) ;

|(p,(qy + ((- 1) * (0. (TOP-REAL n)))))| = 0 by A28, RLVECT_1:16;

then |(p,(qy + (0. (TOP-REAL n))))| = 0 by RLVECT_1:10;

then A29: |(p,qy)| = 0 by RLVECT_1:4;

A30: |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| = (2 * |(qy,p)|) + ((|(qy,qy)| - 1) * |(p,p)|) by EUCLID_2:25

.= |(qy,qy)| - 1 by A5, A29 ;

A31: |(qx,p)| = (1 / (|(qy,qy)| + 1)) * |(((2 * qy) + ((|(qy,qy)| - 1) * p)),p)| by A26, EUCLID_2:19

.= ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) * 1 by A30, XCMPLX_1:75 ;

A32: |(qy,qy)| >= 0 by EUCLID_2:35;

A33: 1 - |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) - ((|(qy,qy)| - 1) / (|(qy,qy)| + 1)) by A31, A32, XCMPLX_1:60

.= ((|(qy,qy)| + 1) - (|(qy,qy)| - 1)) / (|(qy,qy)| + 1) by XCMPLX_1:120

.= 2 / (|(qy,qy)| + 1) ;

A34: 1 / (1 - |(qx,p)|) = (|(qy,qy)| + 1) / 2 by A33, XCMPLX_1:57;

A35: ((|(qy,qy)| + 1) / 2) * qx = (((|(qy,qy)| + 1) / 2) * (1 / (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A26, RLVECT_1:def 7

.= (((|(qy,qy)| + 1) * 1) / (2 * (|(qy,qy)| + 1))) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by XCMPLX_1:76

.= (((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * (1 / 2)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by XCMPLX_1:76

.= (1 * (1 / 2)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A32, XCMPLX_1:60

.= ((1 / 2) * (2 * qy)) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 5

.= (((1 / 2) * 2) * qy) + ((1 / 2) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 7

.= (1 * qy) + (((1 / 2) * (|(qy,qy)| - 1)) * p) by RLVECT_1:def 7

.= qy + (((|(qy,qy)| - 1) / 2) * p) by RLVECT_1:def 8 ;

A36: ((|(qy,qy)| + 1) / 2) * |(qx,p)| = ((|(qy,qy)| + 1) / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) / 2) by A31, XCMPLX_1:85

.= 1 * ((|(qy,qy)| - 1) / 2) by A32, XCMPLX_1:60

.= (|(qy,qy)| - 1) / 2 ;

thus f1 . x = (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| + 1) / 2) * (|(qx,p)| * p)) by A27, A34, RLVECT_1:34

.= (((|(qy,qy)| + 1) / 2) * qx) - (((|(qy,qy)| - 1) / 2) * p) by A36, RLVECT_1:def 7

.= y by A35, RLVECT_4:1 ; :: thesis: verum

assume A38: f1 . x = y ; :: thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x )

hence y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A37, FUNCT_2:5; :: thesis: g1 . y = x

[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qx = x as Point of (TOP-REAL n) by A37;

qx in S by A37;

then A40: y = (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by A38, A2, Def5;

then reconsider qy = y as Point of (TOP-REAL n) ;

A41: qy in TPlane (p,(0. (TOP-REAL n))) by A38, A37, FUNCT_2:5;

A42: g1 . qy = (1 / (|(qy,qy)| + 1)) * ((2 * qy) + ((|(qy,qy)| - 1) * p)) by A41, A18;

reconsider qx1 = qx as Point of (TOP-REAL n1) ;

qx1 in Sphere ((0. (TOP-REAL n)),1) by A37, A1, XBOOLE_0:def 5;

then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;

then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;

then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;

then |.qx.| = 1 by RLVECT_1:4;

then |(qx,qx)| = 1 ^2 by EUCLID_2:4;

then A43: |(qx,qx)| = 1 * 1 by SQUARE_1:def 1;

A44: |((|(qx,p)| * p),(qx - (|(qx,p)| * p)))| = |((|(qx,p)| * p),qx)| - |((|(qx,p)| * p),(|(qx,p)| * p))| by EUCLID_2:27

.= (|(qx,p)| * |(qx,p)|) - |((|(qx,p)| * p),(|(qx,p)| * p))| by EUCLID_2:19

.= (|(qx,p)| * |(qx,p)|) - (|(qx,p)| * |(p,(|(qx,p)| * p))|) by EUCLID_2:19

.= (|(qx,p)| * |(qx,p)|) - (|(qx,p)| * (|(qx,p)| * |(p,p)|)) by EUCLID_2:20

.= 0 by A5 ;

A45: |(qx,(qx - (|(qx,p)| * p)))| = |(qx,qx)| - |(qx,(|(qx,p)| * p))| by EUCLID_2:24

.= 1 - (|(qx,p)| * |(qx,p)|) by A43, EUCLID_2:20 ;

A46: |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))| = |(qx,(qx - (|(qx,p)| * p)))| - |((|(qx,p)| * p),(qx - (|(qx,p)| * p)))| by EUCLID_2:24

.= (1 - (|(qx,p)| * |(qx,p)|)) + 0 by A45, A44 ;

|(qx,p)| <> 1

proof

then A51:
1 - |(qx,p)| <> 0
;
assume A47:
|(qx,p)| = 1
; :: thesis: contradiction

A48: not qx in {p} by A1, A37, XBOOLE_0:def 5;

|(qx,p)| - |(qx,qx)| = 0 by A43, A47;

then A49: |(qx,(p - qx))| = 0 by EUCLID_2:27;

|(p,p)| - |(qx,p)| = 0 by A5, A47;

then A50: |((p - qx),p)| = 0 by EUCLID_2:24;

|((p - qx),(p - qx))| = 0 - 0 by A49, A50, EUCLID_2:24;

then p - qx = 0. (TOP-REAL n) by EUCLID_2:41;

then p = qx by RLVECT_1:21;

hence contradiction by A48, TARSKI:def 1; :: thesis: verum

end;A48: not qx in {p} by A1, A37, XBOOLE_0:def 5;

|(qx,p)| - |(qx,qx)| = 0 by A43, A47;

then A49: |(qx,(p - qx))| = 0 by EUCLID_2:27;

|(p,p)| - |(qx,p)| = 0 by A5, A47;

then A50: |((p - qx),p)| = 0 by EUCLID_2:24;

|((p - qx),(p - qx))| = 0 - 0 by A49, A50, EUCLID_2:24;

then p - qx = 0. (TOP-REAL n) by EUCLID_2:41;

then p = qx by RLVECT_1:21;

hence contradiction by A48, TARSKI:def 1; :: thesis: verum

then A52: (1 - |(qx,p)|) * (1 - |(qx,p)|) <> 0 ;

A53: |(qy,qy)| = (1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),qy)| by A40, EUCLID_2:19

.= (1 / (1 - |(qx,p)|)) * ((1 / (1 - |(qx,p)|)) * |((qx - (|(qx,p)| * p)),(qx - (|(qx,p)| * p)))|) by A40, EUCLID_2:19

.= ((1 / (1 - |(qx,p)|)) * (1 / (1 - |(qx,p)|))) * (1 - (|(qx,p)| * |(qx,p)|)) by A46

.= (1 / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) * (1 - (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:102

.= (1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:99 ;

A54: |(qy,qy)| + 1 = ((1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) + (((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) by A53, A52, XCMPLX_1:60

.= ((1 - (|(qx,p)| * |(qx,p)|)) + ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:62

.= (2 * (1 - |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))

.= 2 * ((1 - |(qx,p)|) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) by XCMPLX_1:74

.= 2 * (((1 - |(qx,p)|) / (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:78

.= 2 * (1 / (1 - |(qx,p)|)) by A51, XCMPLX_1:60

.= (2 * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ;

A55: |(qy,qy)| - 1 = ((1 - (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) - (((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) by A53, A52, XCMPLX_1:60

.= ((1 - (|(qx,p)| * |(qx,p)|)) - ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|))) / ((1 - (2 * |(qx,p)|)) + (|(qx,p)| * |(qx,p)|)) by XCMPLX_1:120

.= ((2 * |(qx,p)|) * (1 - |(qx,p)|)) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))

.= (2 * |(qx,p)|) * ((1 - |(qx,p)|) / ((1 - |(qx,p)|) * (1 - |(qx,p)|))) by XCMPLX_1:74

.= (2 * |(qx,p)|) * (((1 - |(qx,p)|) / (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:78

.= (2 * |(qx,p)|) * (1 / (1 - |(qx,p)|)) by A51, XCMPLX_1:60

.= ((2 * |(qx,p)|) * 1) / (1 - |(qx,p)|) by XCMPLX_1:74 ;

A56: 1 / (|(qy,qy)| + 1) = (1 - |(qx,p)|) / 2 by A54, XCMPLX_1:57;

A57: (|(qy,qy)| - 1) / (|(qy,qy)| + 1) = (2 * |(qx,p)|) / ((1 - |(qx,p)|) * (2 / (1 - |(qx,p)|))) by A54, A55, XCMPLX_1:78

.= (2 * |(qx,p)|) / ((2 * (1 - |(qx,p)|)) / (1 - |(qx,p)|)) by XCMPLX_1:74

.= (2 * |(qx,p)|) / (2 * ((1 - |(qx,p)|) / (1 - |(qx,p)|))) by XCMPLX_1:74

.= (2 * |(qx,p)|) / (2 * 1) by A51, XCMPLX_1:60

.= |(qx,p)| ;

A58: (1 - |(qx,p)|) * qy = ((1 - |(qx,p)|) * (1 / (1 - |(qx,p)|))) * (qx - (|(qx,p)| * p)) by A40, RLVECT_1:def 7

.= (((1 - |(qx,p)|) * 1) / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by XCMPLX_1:74

.= 1 * (qx - (|(qx,p)| * p)) by A51, XCMPLX_1:60

.= qx - (|(qx,p)| * p) by RLVECT_1:def 8 ;

thus g1 . y = ((1 / (|(qy,qy)| + 1)) * (2 * qy)) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by A42, RLVECT_1:def 5

.= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + ((1 / (|(qy,qy)| + 1)) * ((|(qy,qy)| - 1) * p)) by RLVECT_1:def 7

.= (((1 / (|(qy,qy)| + 1)) * 2) * qy) + (((1 / (|(qy,qy)| + 1)) * (|(qy,qy)| - 1)) * p) by RLVECT_1:def 7

.= ((1 - |(qx,p)|) * qy) + (((1 * (|(qy,qy)| - 1)) / (|(qy,qy)| + 1)) * p) by A56, XCMPLX_1:74

.= qx - ((|(qx,p)| * p) - (|(qx,p)| * p)) by A57, A58, RLVECT_1:29

.= qx - (0. (TOP-REAL n)) by RLVECT_1:5

.= qx + ((- 1) * (0. (TOP-REAL n))) by RLVECT_1:16

.= qx + (0. (TOP-REAL n)) by RLVECT_1:10

.= x by RLVECT_1:4 ; :: thesis: verum

( y in [#] (TPlane (p,(0. (TOP-REAL n)))) iff ex x being object st

( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) )

proof

then A61:
rng (stereographic_projection (S,p)) = [#] (TPlane (p,(0. (TOP-REAL n))))
by FUNCT_1:def 3;
let y be object ; :: thesis: ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) iff ex x being object st

( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) )

thus y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A60, FUNCT_2:5; :: thesis: verum

end;( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) )

hereby :: thesis: ( ex x being object st

( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) implies y in [#] (TPlane (p,(0. (TOP-REAL n)))) )

given x being object such that A60:
( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x )
; :: thesis: y in [#] (TPlane (p,(0. (TOP-REAL n))))( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x ) implies y in [#] (TPlane (p,(0. (TOP-REAL n)))) )

assume A59:
y in [#] (TPlane (p,(0. (TOP-REAL n))))
; :: thesis: ex x being object st

( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x )

reconsider x = g . y as object ;

take x = x; :: thesis: ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x )

thus x in dom (stereographic_projection (S,p)) by A22, A3, A59; :: thesis: y = (stereographic_projection (S,p)) . x

thus y = (stereographic_projection (S,p)) . x by A59, A22; :: thesis: verum

end;( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x )

reconsider x = g . y as object ;

take x = x; :: thesis: ( x in dom (stereographic_projection (S,p)) & y = (stereographic_projection (S,p)) . x )

thus x in dom (stereographic_projection (S,p)) by A22, A3, A59; :: thesis: y = (stereographic_projection (S,p)) . x

thus y = (stereographic_projection (S,p)) . x by A59, A22; :: thesis: verum

thus y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A60, FUNCT_2:5; :: thesis: verum

A62: stereographic_projection (S,p) is one-to-one

proof

A65:
stereographic_projection (S,p) is continuous
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (stereographic_projection (S,p)) or not x2 in dom (stereographic_projection (S,p)) or not (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 or x1 = x2 )

assume A63: ( x1 in dom (stereographic_projection (S,p)) & x2 in dom (stereographic_projection (S,p)) ) ; :: thesis: ( not (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 or x1 = x2 )

assume A64: (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 ; :: thesis: x1 = x2

( g1 . ((stereographic_projection (S,p)) . x1) = x1 & g1 . ((stereographic_projection (S,p)) . x2) = x2 ) by A63, A22;

hence x1 = x2 by A64; :: thesis: verum

end;assume A63: ( x1 in dom (stereographic_projection (S,p)) & x2 in dom (stereographic_projection (S,p)) ) ; :: thesis: ( not (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 or x1 = x2 )

assume A64: (stereographic_projection (S,p)) . x1 = (stereographic_projection (S,p)) . x2 ; :: thesis: x1 = x2

( g1 . ((stereographic_projection (S,p)) . x1) = x1 & g1 . ((stereographic_projection (S,p)) . x2) = x2 ) by A63, A22;

hence x1 = x2 by A64; :: thesis: verum

proof

A96:
g is continuous
A66:
[#] S c= [#] (TOP-REAL n)
by PRE_TOPC:def 4;

set f0 = InnerProduct p;

consider f1 being Function of (TOP-REAL n1),R^1 such that

A67: ( ( for q being Point of (TOP-REAL n) holds f1 . q = 1 ) & f1 is continuous ) by JGRAPH_2:20;

consider f2 being Function of (TOP-REAL n),R^1 such that

A68: ( ( for q being Point of (TOP-REAL n)

for r1, r2 being Real st f1 . q = r1 & (InnerProduct p) . q = r2 holds

f2 . q = r1 - r2 ) & f2 is continuous ) by A67, JGRAPH_2:21;

reconsider f2 = f2 as continuous Function of (TOP-REAL n),R^1 by A68;

reconsider S1 = S as non empty TopSpace by A20, A1, A19, XBOOLE_0:def 5;

set f3 = f2 | S1;

A69: for q being Point of (TOP-REAL n) st q in S1 holds

(f2 | S1) . q = 1 - |(q,p)|

A80: ( ( for q being Point of S1

for r1 being Real st (f2 | S1) . q = r1 holds

f4 . q = 1 / r1 ) & f4 is continuous ) by JGRAPH_2:26;

consider f5 being Function of S1,(TOP-REAL n1) such that

A81: ( ( for a being Point of S1

for b being Point of (TOP-REAL n)

for r being Real st a = b & f4 . a = r holds

f5 . b = r * b ) & f5 is continuous ) by A80, MFOLD_1:2;

set f6 = (InnerProduct p) | S1;

A82: for q being Point of (TOP-REAL n) st q in S1 holds

((InnerProduct p) | S1) . q = |(q,p)|

A86: ( ( for q being Point of S1

for r1, r2 being Real st ((InnerProduct p) | S1) . q = r1 & (f2 | S1) . q = r2 holds

f7 . q = r1 / r2 ) & f7 is continuous ) by A73, JGRAPH_2:27;

reconsider p1 = - p as Point of (TOP-REAL n1) ;

consider f8 being Function of S1,(TOP-REAL n1) such that

A87: ( ( for r being Point of S1 holds f8 . r = (f7 . r) * p1 ) & f8 is continuous ) by A86, JGRAPH_6:9;

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

A88: ( ( for r being Point of S1 holds f9 . r = (f5 . r) + (f8 . r) ) & f9 is continuous ) by A87, A81, JGRAPH_6:12;

A89: dom (stereographic_projection (S,p)) = [#] S by FUNCT_2:def 1

.= dom f9 by FUNCT_2:def 1 ;

for x being object st x in dom (stereographic_projection (S,p)) holds

(stereographic_projection (S,p)) . x = f9 . x

end;set f0 = InnerProduct p;

consider f1 being Function of (TOP-REAL n1),R^1 such that

A67: ( ( for q being Point of (TOP-REAL n) holds f1 . q = 1 ) & f1 is continuous ) by JGRAPH_2:20;

consider f2 being Function of (TOP-REAL n),R^1 such that

A68: ( ( for q being Point of (TOP-REAL n)

for r1, r2 being Real st f1 . q = r1 & (InnerProduct p) . q = r2 holds

f2 . q = r1 - r2 ) & f2 is continuous ) by A67, JGRAPH_2:21;

reconsider f2 = f2 as continuous Function of (TOP-REAL n),R^1 by A68;

reconsider S1 = S as non empty TopSpace by A20, A1, A19, XBOOLE_0:def 5;

set f3 = f2 | S1;

A69: for q being Point of (TOP-REAL n) st q in S1 holds

(f2 | S1) . q = 1 - |(q,p)|

proof

A73:
for q being Point of S1 holds (f2 | S1) . q <> 0
let q be Point of (TOP-REAL n); :: thesis: ( q in S1 implies (f2 | S1) . q = 1 - |(q,p)| )

assume B70: q in S1 ; :: thesis: (f2 | S1) . q = 1 - |(q,p)|

A71: [#] S1 c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

( (InnerProduct p) . q = |(q,p)| & f1 . q = 1 ) by Def1, A67;

then A72: f2 . q = 1 - |(q,p)| by A68;

thus (f2 | S1) . q = (f2 | the carrier of S1) . q by A71, TMAP_1:def 3

.= 1 - |(q,p)| by A72, B70, FUNCT_1:49 ; :: thesis: verum

end;assume B70: q in S1 ; :: thesis: (f2 | S1) . q = 1 - |(q,p)|

A71: [#] S1 c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

( (InnerProduct p) . q = |(q,p)| & f1 . q = 1 ) by Def1, A67;

then A72: f2 . q = 1 - |(q,p)| by A68;

thus (f2 | S1) . q = (f2 | the carrier of S1) . q by A71, TMAP_1:def 3

.= 1 - |(q,p)| by A72, B70, FUNCT_1:49 ; :: thesis: verum

proof

then consider f4 being Function of S1,R^1 such that
let q be Point of S1; :: thesis: (f2 | S1) . q <> 0

reconsider qx = q as Point of (TOP-REAL n) by A66;

reconsider qx1 = qx as Point of (TOP-REAL n1) ;

qx1 in Sphere ((0. (TOP-REAL n)),1) by A1, XBOOLE_0:def 5;

then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;

then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;

then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;

then |.qx.| = 1 by RLVECT_1:4;

then |(qx,qx)| = 1 ^2 by EUCLID_2:4;

then A74: |(qx,qx)| = 1 * 1 by SQUARE_1:def 1;

|(qx,p)| <> 1

qx in S1 ;

hence (f2 | S1) . q <> 0 by A69, A79; :: thesis: verum

end;reconsider qx = q as Point of (TOP-REAL n) by A66;

reconsider qx1 = qx as Point of (TOP-REAL n1) ;

qx1 in Sphere ((0. (TOP-REAL n)),1) by A1, XBOOLE_0:def 5;

then |.(qx1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;

then |.(qx1 + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:16;

then |.(qx1 + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:10;

then |.qx.| = 1 by RLVECT_1:4;

then |(qx,qx)| = 1 ^2 by EUCLID_2:4;

then A74: |(qx,qx)| = 1 * 1 by SQUARE_1:def 1;

|(qx,p)| <> 1

proof

then A79:
1 - |(qx,p)| <> 0
;
assume A75:
|(qx,p)| = 1
; :: thesis: contradiction

A76: not qx in {p} by A1, XBOOLE_0:def 5;

|(qx,p)| - |(qx,qx)| = 0 by A74, A75;

then A77: |(qx,(p - qx))| = 0 by EUCLID_2:27;

|(p,p)| - |(qx,p)| = 0 by A5, A75;

then A78: |((p - qx),p)| = 0 by EUCLID_2:24;

|((p - qx),(p - qx))| = 0 - 0 by A77, A78, EUCLID_2:24;

then p - qx = 0. (TOP-REAL n) by EUCLID_2:41;

then p = qx by RLVECT_1:21;

hence contradiction by A76, TARSKI:def 1; :: thesis: verum

end;A76: not qx in {p} by A1, XBOOLE_0:def 5;

|(qx,p)| - |(qx,qx)| = 0 by A74, A75;

then A77: |(qx,(p - qx))| = 0 by EUCLID_2:27;

|(p,p)| - |(qx,p)| = 0 by A5, A75;

then A78: |((p - qx),p)| = 0 by EUCLID_2:24;

|((p - qx),(p - qx))| = 0 - 0 by A77, A78, EUCLID_2:24;

then p - qx = 0. (TOP-REAL n) by EUCLID_2:41;

then p = qx by RLVECT_1:21;

hence contradiction by A76, TARSKI:def 1; :: thesis: verum

qx in S1 ;

hence (f2 | S1) . q <> 0 by A69, A79; :: thesis: verum

A80: ( ( for q being Point of S1

for r1 being Real st (f2 | S1) . q = r1 holds

f4 . q = 1 / r1 ) & f4 is continuous ) by JGRAPH_2:26;

consider f5 being Function of S1,(TOP-REAL n1) such that

A81: ( ( for a being Point of S1

for b being Point of (TOP-REAL n)

for r being Real st a = b & f4 . a = r holds

f5 . b = r * b ) & f5 is continuous ) by A80, MFOLD_1:2;

set f6 = (InnerProduct p) | S1;

A82: for q being Point of (TOP-REAL n) st q in S1 holds

((InnerProduct p) | S1) . q = |(q,p)|

proof

consider f7 being Function of S1,R^1 such that
let q be Point of (TOP-REAL n); :: thesis: ( q in S1 implies ((InnerProduct p) | S1) . q = |(q,p)| )

assume B83: q in S1 ; :: thesis: ((InnerProduct p) | S1) . q = |(q,p)|

A84: [#] S1 c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

A85: (InnerProduct p) . q = |(q,p)| by Def1;

thus ((InnerProduct p) | S1) . q = ((InnerProduct p) | the carrier of S1) . q by A84, TMAP_1:def 3

.= |(q,p)| by A85, B83, FUNCT_1:49 ; :: thesis: verum

end;assume B83: q in S1 ; :: thesis: ((InnerProduct p) | S1) . q = |(q,p)|

A84: [#] S1 c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

A85: (InnerProduct p) . q = |(q,p)| by Def1;

thus ((InnerProduct p) | S1) . q = ((InnerProduct p) | the carrier of S1) . q by A84, TMAP_1:def 3

.= |(q,p)| by A85, B83, FUNCT_1:49 ; :: thesis: verum

A86: ( ( for q being Point of S1

for r1, r2 being Real st ((InnerProduct p) | S1) . q = r1 & (f2 | S1) . q = r2 holds

f7 . q = r1 / r2 ) & f7 is continuous ) by A73, JGRAPH_2:27;

reconsider p1 = - p as Point of (TOP-REAL n1) ;

consider f8 being Function of S1,(TOP-REAL n1) such that

A87: ( ( for r being Point of S1 holds f8 . r = (f7 . r) * p1 ) & f8 is continuous ) by A86, JGRAPH_6:9;

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

A88: ( ( for r being Point of S1 holds f9 . r = (f5 . r) + (f8 . r) ) & f9 is continuous ) by A87, A81, JGRAPH_6:12;

A89: dom (stereographic_projection (S,p)) = [#] S by FUNCT_2:def 1

.= dom f9 by FUNCT_2:def 1 ;

for x being object st x in dom (stereographic_projection (S,p)) holds

(stereographic_projection (S,p)) . x = f9 . x

proof

hence
stereographic_projection (S,p) is continuous
by A88, A89, FUNCT_1:2, PRE_TOPC:27; :: thesis: verum
let x be object ; :: thesis: ( x in dom (stereographic_projection (S,p)) implies (stereographic_projection (S,p)) . x = f9 . x )

assume A90: x in dom (stereographic_projection (S,p)) ; :: thesis: (stereographic_projection (S,p)) . x = f9 . x

then reconsider qx = x as Point of (TOP-REAL n) by A66;

A91: qx in S by A90;

reconsider r = qx as Point of S1 by A90;

A92: (f2 | S1) . r = 1 - |(qx,p)| by A69, A91;

A93: f4 . r = 1 / (1 - |(qx,p)|) by A92, A80;

A94: ((InnerProduct p) | S1) . r = |(qx,p)| by A82, A91;

A95: f8 . r = (f7 . r) * (- p) by A87

.= (|(qx,p)| / (1 - |(qx,p)|)) * (- p) by A92, A94, A86 ;

f9 . x = (f5 . r) + (f8 . r) by A88

.= ((1 / (1 - |(qx,p)|)) * qx) + (((1 * |(qx,p)|) / (1 - |(qx,p)|)) * (- p)) by A93, A81, A95

.= ((1 / (1 - |(qx,p)|)) * qx) + (((1 / (1 - |(qx,p)|)) * |(qx,p)|) * (- p)) by XCMPLX_1:74

.= ((1 / (1 - |(qx,p)|)) * qx) + ((1 / (1 - |(qx,p)|)) * (|(qx,p)| * (- p))) by RLVECT_1:def 7

.= (1 / (1 - |(qx,p)|)) * (qx + (|(qx,p)| * (- p))) by RLVECT_1:def 5

.= (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by RLVECT_1:25 ;

hence (stereographic_projection (S,p)) . x = f9 . x by A91, A2, Def5; :: thesis: verum

end;assume A90: x in dom (stereographic_projection (S,p)) ; :: thesis: (stereographic_projection (S,p)) . x = f9 . x

then reconsider qx = x as Point of (TOP-REAL n) by A66;

A91: qx in S by A90;

reconsider r = qx as Point of S1 by A90;

A92: (f2 | S1) . r = 1 - |(qx,p)| by A69, A91;

A93: f4 . r = 1 / (1 - |(qx,p)|) by A92, A80;

A94: ((InnerProduct p) | S1) . r = |(qx,p)| by A82, A91;

A95: f8 . r = (f7 . r) * (- p) by A87

.= (|(qx,p)| / (1 - |(qx,p)|)) * (- p) by A92, A94, A86 ;

f9 . x = (f5 . r) + (f8 . r) by A88

.= ((1 / (1 - |(qx,p)|)) * qx) + (((1 * |(qx,p)|) / (1 - |(qx,p)|)) * (- p)) by A93, A81, A95

.= ((1 / (1 - |(qx,p)|)) * qx) + (((1 / (1 - |(qx,p)|)) * |(qx,p)|) * (- p)) by XCMPLX_1:74

.= ((1 / (1 - |(qx,p)|)) * qx) + ((1 / (1 - |(qx,p)|)) * (|(qx,p)| * (- p))) by RLVECT_1:def 7

.= (1 / (1 - |(qx,p)|)) * (qx + (|(qx,p)| * (- p))) by RLVECT_1:def 5

.= (1 / (1 - |(qx,p)|)) * (qx - (|(qx,p)| * p)) by RLVECT_1:25 ;

hence (stereographic_projection (S,p)) . x = f9 . x by A91, A2, Def5; :: thesis: verum

proof

reconsider f2 = f1 as [#] (TPlane (p,(0. (TOP-REAL n)))) -valued Relation ;
consider g0 being Function of (TOP-REAL n1),R^1 such that

A98: ( ( for q being Point of (TOP-REAL n1) holds g0 . q = |.q.| ) & g0 is continuous ) by JORDAN2C:84;

consider g1 being Function of (TOP-REAL n),R^1 such that

A99: ( ( for q being Point of (TOP-REAL n)

for r1 being Real st g0 . q = r1 holds

g1 . q = r1 * r1 ) & g1 is continuous ) by A98, JGRAPH_2:22;

consider g2 being Function of (TOP-REAL n),R^1 such that

A100: ( ( for q being Point of (TOP-REAL n)

for r1 being Real st g1 . q = r1 holds

g2 . q = r1 + 1 ) & g2 is continuous ) by A99, JGRAPH_2:24;

consider g3 being Function of (TOP-REAL n),R^1 such that

A101: ( ( for q being Point of (TOP-REAL n)

for r1 being Real st g1 . q = r1 holds

g3 . q = r1 + (- 1) ) & g3 is continuous ) by A99, JGRAPH_2:24;

consider g4 being Function of (TOP-REAL n),R^1 such that

A102: ( ( for q being Point of (TOP-REAL n) holds g4 . q = 2 ) & g4 is continuous ) by JGRAPH_2:20;

A103: for q being Point of (TOP-REAL n) holds g2 . q <> 0

A104: ( ( for q being Point of (TOP-REAL n)

for r1, r2 being Real st g4 . q = r1 & g2 . q = r2 holds

g5 . q = r1 / r2 ) & g5 is continuous ) by A102, A100, JGRAPH_2:27;

reconsider g6 = g5 | (TPlane (p,(0. (TOP-REAL n)))) as continuous Function of (TPlane (p,(0. (TOP-REAL n)))),R^1 by A104;

consider g7 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that

A105: ( ( for a being Point of (TPlane (p,(0. (TOP-REAL n))))

for b being Point of (TOP-REAL n)

for r being Real st a = b & g6 . a = r holds

g7 . b = r * b ) & g7 is continuous ) by MFOLD_1:2;

consider g8 being Function of (TOP-REAL n),R^1 such that

A106: ( ( for q being Point of (TOP-REAL n)

for r1, r2 being Real st g3 . q = r1 & g2 . q = r2 holds

g8 . q = r1 / r2 ) & g8 is continuous ) by A103, A100, A101, JGRAPH_2:27;

reconsider p1 = p as Point of (TOP-REAL n1) ;

reconsider g9 = g8 | (TPlane (p,(0. (TOP-REAL n)))) as continuous Function of (TPlane (p,(0. (TOP-REAL n)))),R^1 by A106;

consider g10 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that

A107: ( ( for r being Point of (TPlane (p,(0. (TOP-REAL n)))) holds g10 . r = (g9 . r) * p1 ) & g10 is continuous ) by JGRAPH_6:9;

consider g11 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that

A108: ( ( for r being Point of (TPlane (p,(0. (TOP-REAL n)))) holds g11 . r = (g7 . r) + (g10 . r) ) & g11 is continuous ) by A105, A107, JGRAPH_6:12;

A109: dom g = [#] (TPlane (p,(0. (TOP-REAL n)))) by A21, FUNCT_2:def 1

.= dom g11 by FUNCT_2:def 1 ;

for x being object st x in dom g holds

g . x = g11 . x

end;A98: ( ( for q being Point of (TOP-REAL n1) holds g0 . q = |.q.| ) & g0 is continuous ) by JORDAN2C:84;

consider g1 being Function of (TOP-REAL n),R^1 such that

A99: ( ( for q being Point of (TOP-REAL n)

for r1 being Real st g0 . q = r1 holds

g1 . q = r1 * r1 ) & g1 is continuous ) by A98, JGRAPH_2:22;

consider g2 being Function of (TOP-REAL n),R^1 such that

A100: ( ( for q being Point of (TOP-REAL n)

for r1 being Real st g1 . q = r1 holds

g2 . q = r1 + 1 ) & g2 is continuous ) by A99, JGRAPH_2:24;

consider g3 being Function of (TOP-REAL n),R^1 such that

A101: ( ( for q being Point of (TOP-REAL n)

for r1 being Real st g1 . q = r1 holds

g3 . q = r1 + (- 1) ) & g3 is continuous ) by A99, JGRAPH_2:24;

consider g4 being Function of (TOP-REAL n),R^1 such that

A102: ( ( for q being Point of (TOP-REAL n) holds g4 . q = 2 ) & g4 is continuous ) by JGRAPH_2:20;

A103: for q being Point of (TOP-REAL n) holds g2 . q <> 0

proof

then consider g5 being Function of (TOP-REAL n),R^1 such that
let q be Point of (TOP-REAL n); :: thesis: g2 . q <> 0

g0 . q = |.q.| by A98;

then g1 . q = |.q.| * |.q.| by A99;

then g2 . q = (|.q.| * |.q.|) + 1 by A100;

hence g2 . q <> 0 ; :: thesis: verum

end;g0 . q = |.q.| by A98;

then g1 . q = |.q.| * |.q.| by A99;

then g2 . q = (|.q.| * |.q.|) + 1 by A100;

hence g2 . q <> 0 ; :: thesis: verum

A104: ( ( for q being Point of (TOP-REAL n)

for r1, r2 being Real st g4 . q = r1 & g2 . q = r2 holds

g5 . q = r1 / r2 ) & g5 is continuous ) by A102, A100, JGRAPH_2:27;

reconsider g6 = g5 | (TPlane (p,(0. (TOP-REAL n)))) as continuous Function of (TPlane (p,(0. (TOP-REAL n)))),R^1 by A104;

consider g7 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that

A105: ( ( for a being Point of (TPlane (p,(0. (TOP-REAL n))))

for b being Point of (TOP-REAL n)

for r being Real st a = b & g6 . a = r holds

g7 . b = r * b ) & g7 is continuous ) by MFOLD_1:2;

consider g8 being Function of (TOP-REAL n),R^1 such that

A106: ( ( for q being Point of (TOP-REAL n)

for r1, r2 being Real st g3 . q = r1 & g2 . q = r2 holds

g8 . q = r1 / r2 ) & g8 is continuous ) by A103, A100, A101, JGRAPH_2:27;

reconsider p1 = p as Point of (TOP-REAL n1) ;

reconsider g9 = g8 | (TPlane (p,(0. (TOP-REAL n)))) as continuous Function of (TPlane (p,(0. (TOP-REAL n)))),R^1 by A106;

consider g10 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that

A107: ( ( for r being Point of (TPlane (p,(0. (TOP-REAL n)))) holds g10 . r = (g9 . r) * p1 ) & g10 is continuous ) by JGRAPH_6:9;

consider g11 being Function of (TPlane (p,(0. (TOP-REAL n)))),(TOP-REAL n1) such that

A108: ( ( for r being Point of (TPlane (p,(0. (TOP-REAL n)))) holds g11 . r = (g7 . r) + (g10 . r) ) & g11 is continuous ) by A105, A107, JGRAPH_6:12;

A109: dom g = [#] (TPlane (p,(0. (TOP-REAL n)))) by A21, FUNCT_2:def 1

.= dom g11 by FUNCT_2:def 1 ;

for x being object st x in dom g holds

g . x = g11 . x

proof

hence
g is continuous
by A108, A109, FUNCT_1:2, PRE_TOPC:27; :: thesis: verum
let x be object ; :: thesis: ( x in dom g implies g . x = g11 . x )

assume A110: x in dom g ; :: thesis: g . x = g11 . x

[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qx = x as Point of (TOP-REAL n) by A110;

A112: qx in TPlane (p,(0. (TOP-REAL n))) by A110;

reconsider r = qx as Point of (TPlane (p,(0. (TOP-REAL n)))) by A110;

A113: [#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

A114: g0 . qx = |.qx.| by A98;

A115: g1 . qx = |.qx.| * |.qx.| by A99, A114

.= |.qx.| ^2 by SQUARE_1:def 1

.= |(qx,qx)| by EUCLID_2:4 ;

A116: g2 . qx = |(qx,qx)| + 1 by A100, A115;

A117: g4 . qx = 2 by A102;

A118: g6 . qx = (g5 | the carrier of (TPlane (p,(0. (TOP-REAL n))))) . qx by A113, TMAP_1:def 3

.= g5 . qx by A110, FUNCT_1:49

.= 2 / (|(qx,qx)| + 1) by A104, A117, A116 ;

A119: g3 . qx = |(qx,qx)| + (- 1) by A101, A115;

A120: g9 . qx = (g8 | the carrier of (TPlane (p,(0. (TOP-REAL n))))) . qx by A113, TMAP_1:def 3

.= g8 . qx by A110, FUNCT_1:49

.= (|(qx,qx)| - 1) / (|(qx,qx)| + 1) by A116, A119, A106 ;

A121: g7 . r = (2 / (|(qx,qx)| + 1)) * qx by A105, A118;

g11 . x = (g7 . r) + (g10 . r) by A108

.= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 * (|(qx,qx)| - 1)) / (|(qx,qx)| + 1)) * p) by A120, A107, A121

.= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 / (|(qx,qx)| + 1)) * (|(qx,qx)| - 1)) * p) by XCMPLX_1:74

.= (((1 / (|(qx,qx)| + 1)) * 2) * qx) + (((1 / (|(qx,qx)| + 1)) * (|(qx,qx)| - 1)) * p) by XCMPLX_1:74

.= (((1 / (|(qx,qx)| + 1)) * 2) * qx) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 7

.= ((1 / (|(qx,qx)| + 1)) * (2 * qx)) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 7

.= (1 / (|(qx,qx)| + 1)) * ((2 * qx) + ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 5 ;

hence g . x = g11 . x by A18, A112; :: thesis: verum

end;assume A110: x in dom g ; :: thesis: g . x = g11 . x

[#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

then reconsider qx = x as Point of (TOP-REAL n) by A110;

A112: qx in TPlane (p,(0. (TOP-REAL n))) by A110;

reconsider r = qx as Point of (TPlane (p,(0. (TOP-REAL n)))) by A110;

A113: [#] (TPlane (p,(0. (TOP-REAL n)))) c= [#] (TOP-REAL n) by PRE_TOPC:def 4;

A114: g0 . qx = |.qx.| by A98;

A115: g1 . qx = |.qx.| * |.qx.| by A99, A114

.= |.qx.| ^2 by SQUARE_1:def 1

.= |(qx,qx)| by EUCLID_2:4 ;

A116: g2 . qx = |(qx,qx)| + 1 by A100, A115;

A117: g4 . qx = 2 by A102;

A118: g6 . qx = (g5 | the carrier of (TPlane (p,(0. (TOP-REAL n))))) . qx by A113, TMAP_1:def 3

.= g5 . qx by A110, FUNCT_1:49

.= 2 / (|(qx,qx)| + 1) by A104, A117, A116 ;

A119: g3 . qx = |(qx,qx)| + (- 1) by A101, A115;

A120: g9 . qx = (g8 | the carrier of (TPlane (p,(0. (TOP-REAL n))))) . qx by A113, TMAP_1:def 3

.= g8 . qx by A110, FUNCT_1:49

.= (|(qx,qx)| - 1) / (|(qx,qx)| + 1) by A116, A119, A106 ;

A121: g7 . r = (2 / (|(qx,qx)| + 1)) * qx by A105, A118;

g11 . x = (g7 . r) + (g10 . r) by A108

.= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 * (|(qx,qx)| - 1)) / (|(qx,qx)| + 1)) * p) by A120, A107, A121

.= (((1 * 2) / (|(qx,qx)| + 1)) * qx) + (((1 / (|(qx,qx)| + 1)) * (|(qx,qx)| - 1)) * p) by XCMPLX_1:74

.= (((1 / (|(qx,qx)| + 1)) * 2) * qx) + (((1 / (|(qx,qx)| + 1)) * (|(qx,qx)| - 1)) * p) by XCMPLX_1:74

.= (((1 / (|(qx,qx)| + 1)) * 2) * qx) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 7

.= ((1 / (|(qx,qx)| + 1)) * (2 * qx)) + ((1 / (|(qx,qx)| + 1)) * ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 7

.= (1 / (|(qx,qx)| + 1)) * ((2 * qx) + ((|(qx,qx)| - 1) * p)) by RLVECT_1:def 5 ;

hence g . x = g11 . x by A18, A112; :: thesis: verum

f2 is onto by A61, FUNCT_2:def 3;

then A122: f1 " = f1 " by A62, TOPS_2:def 4;

g1 = f1 " by A61, A62, A22, A21, FUNCT_2:28;

hence stereographic_projection (S,p) is being_homeomorphism by A3, A61, A62, A65, A96, A122, TOPS_2:def 5; :: thesis: verum