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₁[ 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₁[x,y] )

proof

let x be object ; :: thesis: ( x in [#] (TPlane (p,(0. (TOP-REAL n)))) implies ex y being object st
( y in [#] S & S₁[x,y] ) )
assume A7: x in [#] (TPlane (p,(0. (TOP-REAL n)))) ; :: thesis: ex y being object st
( y in [#] S & S₁[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₁[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}

proof

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;

reconsider y1 = (1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p)) as Point of (TOP-REAL n1) ;
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₁[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))]
thus S₁[x,(1 / (|(q,q)| + 1)) * ((2 * q) + ((|(q,q)| - 1) * p))] ; :: thesis: verum

end;

consider g1 being Function of ([#] (TPlane (p,(0. (TOP-REAL n))))),([#] S) such that
A18: for x being object st x in [#] (TPlane (p,(0. (TOP-REAL n)))) holds
S₁[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 ) )

proof

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

hereby :: thesis: ( x in [#] S & f1 . x = y implies ( 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 A37: x in [#] S ; :: thesis: ( not f1 . x = y or ( y in [#] (TPlane (p,(0. (TOP-REAL n)))) & g1 . y = x ) )
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

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;

then A51: 1 - |(qx,p)| <> 0 ;
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;

for y being object holds
( 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

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

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

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;

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))))
thus y in [#] (TPlane (p,(0. (TOP-REAL n)))) by A60, FUNCT_2:5; :: thesis: verum

end;

then A61: rng (stereographic_projection (S,p)) = [#] (TPlane (p,(0. (TOP-REAL n)))) by FUNCT_1:def 3;
A62: stereographic_projection (S,p) is one-to-one

proof

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;

A65: stereographic_projection (S,p) is continuous

proof

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

proof

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;

A73: for q being Point of S1 holds (f2 | S1) . q <> 0

proof

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

proof

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;

then A79: 1 - |(qx,p)| <> 0 ;
qx in S1 ;
hence (f2 | S1) . q <> 0 by A69, A79; :: thesis: verum

end;

then consider f4 being Function of S1,R^1 such that
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

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;

consider f7 being Function of S1,R^1 such that
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

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;

hence stereographic_projection (S,p) is continuous by A88, A89, FUNCT_1:2, PRE_TOPC:27; :: thesis: verum

end;

A96: g is continuous

proof

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

proof

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;

then consider g5 being Function of (TOP-REAL n),R^1 such that
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

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;

hence g is continuous by A108, A109, FUNCT_1:2, PRE_TOPC:27; :: thesis: verum

end;

reconsider f2 = f1 as [#] (TPlane (p,(0. (TOP-REAL n)))) -valued Relation ;
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