:: Fan Homeomorphisms in the Plane
::  by Yatsuka Nakamura
::
:: Received January 8, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, PRE_TOPC, EUCLID, SUPINF_2, COMPLEX1, XXREAL_0, CARD_1,
      XBOOLE_0, FUNCT_1, TOPMETR, SUBSET_1, ORDINAL2, PARTFUN1, RCOMP_1,
      REAL_1, TARSKI, STRUCT_0, RELAT_1, ARYTM_3, TOPS_2, ARYTM_1, SQUARE_1,
      NAT_1, METRIC_1, XXREAL_2, PCOMPS_1, MCART_1, FUNCT_4, JGRAPH_4, FUNCT_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, COMPLEX1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1,
      STRUCT_0, PARTFUN1, TOPMETR, RLVECT_1, EUCLID, COMPTS_1, TOPS_2,
      METRIC_1, PCOMPS_1, SQUARE_1, TBSP_1, PSCOMP_1, PRE_TOPC, RLTOPSP1,
      FUNCT_4, XXREAL_0;
 constructors FUNCT_4, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, TOPS_2, COMPTS_1,
      TBSP_1, TOPMETR, PSCOMP_1, FUNCSDOM, PCOMPS_1;
 registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED,
      STRUCT_0, PRE_TOPC, EUCLID, TOPMETR, TOPREAL1, PSCOMP_1, FUNCT_2,
      COMPTS_1, TBSP_1, RELSET_1, FUNCT_1, JORDAN2C, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

reserve a for Real;
reserve p,q for Point of TOP-REAL 2;

theorem :: JGRAPH_4:1
  for X being non empty TopStruct, g being Function of X,R^1, B
  being Subset of X, a being Real st g is continuous & B = {p where p is
  Point of X: g/.p > a } holds B is open;

theorem :: JGRAPH_4:2
  for X being non empty TopStruct, g being Function of X,R^1,B
being Subset of X,
  a being Real st g is continuous & B={p where p is Point of X
  : g/.p < a } holds B is open;

theorem :: JGRAPH_4:3
  for f being Function of TOP-REAL 2,TOP-REAL 2 st f is continuous
  one-to-one & rng f=[#](TOP-REAL 2) & (for p2 being Point of TOP-REAL 2 ex K
being non empty compact Subset of TOP-REAL 2 st K = f.:K & (ex V2 being Subset
  of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & f.p2 in V2)) holds f is
  being_homeomorphism;

theorem :: JGRAPH_4:4
  for X being non empty TopSpace, f1,f2 being Function of X,R^1,a,b
being Real st f1 is continuous & f2 is continuous & b<>0 & (for q being
  Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being
Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=(r1/r2-a)/b)
  & g is continuous;

theorem :: JGRAPH_4:5
  for X being non empty TopSpace, f1,f2 being Function of X,R^1,
      a,b being Real
  st f1 is continuous & f2 is continuous & b<>0 & (for q being Point
of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p being Point of
  X,r1,r2 being Real
   st f1.p=r1 & f2.p=r2 holds g.p=r2*((r1/r2-a)/b)) & g is
  continuous;

theorem :: JGRAPH_4:6
  for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1
  being Real st f1.p=r1 holds g.p=r1^2) & g is continuous;

theorem :: JGRAPH_4:7
  for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1
  being Real st f1.p=r1 holds g.p=|.r1.|) & g is continuous;

theorem :: JGRAPH_4:8
  for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous holds ex g being Function of X,R^1 st (for p being Point of X,r1
  being Real st f1.p=r1 holds g.p=-r1) & g is continuous;

theorem :: JGRAPH_4:9
  for X being non empty TopSpace, f1,f2 being Function of X,R^1,a,
  b being Real st f1 is continuous & f2 is continuous & b<>0 & (for q
  being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p
being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p= r2*(-
  sqrt(|.1-((r1/r2-a)/b)^2.|))) & g is continuous;

theorem :: JGRAPH_4:10
  for X being non empty TopSpace, f1,f2 being Function of X,R^1,a,
  b being Real st f1 is continuous & f2 is continuous & b<>0 & (for q
  being Point of X holds f2.q<>0) holds ex g being Function of X,R^1 st (for p
  being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p= r2*(
  sqrt(|.1-((r1/r2-a)/b)^2.|))) & g is continuous;

definition
  let n be Nat;
  func n NormF -> Function of TOP-REAL n, R^1 means
:: JGRAPH_4:def 1

  for q being Point of TOP-REAL n holds it.q=|.q.|;
end;

theorem :: JGRAPH_4:11
  for n being Nat holds dom (n NormF)=the carrier of TOP-REAL
  n & dom (n NormF)=REAL n;

theorem :: JGRAPH_4:12
  for n being Nat holds n NormF is continuous;

registration
  let n be Nat;
  cluster n NormF -> continuous;
end;

theorem :: JGRAPH_4:13
  for n being Element of NAT,K0 being Subset of TOP-REAL n, f
being Function of (TOP-REAL n)|K0,R^1 st (for p being Point of (TOP-REAL n)|K0
  holds f.p=(n NormF).p) holds f is continuous;

theorem :: JGRAPH_4:14
  for n being Element of NAT,p being Point of Euclid n,r being
Real, B being Subset of TOP-REAL n st B=cl_Ball(p,r)
holds B is bounded closed;

theorem :: JGRAPH_4:15
  for p being Point of Euclid 2,r being Real, B being Subset of
  TOP-REAL 2 st B=cl_Ball(p,r) holds B is compact;

begin :: Fan Morphism for West

definition
  let s be Real, q be Point of TOP-REAL 2;
  func FanW(s,q) -> Point of TOP-REAL 2 equals
:: JGRAPH_4:def 2

  |.q.|*|[-sqrt(1-((q`2/|.
q.|-s)/(1-s))^2), (q`2/|.q.|-s)/(1-s)]| if q`2/|.q.|>=s & q`1<0, |.q.|*|[-sqrt(
  1-((q`2/|.q.|-s)/(1+s))^2), (q`2/|.q.|-s)/(1+s)]| if q`2/|.q.|<s & q`1<0
  otherwise q;
end;

definition
  let s be Real;
  func s-FanMorphW -> Function of TOP-REAL 2, TOP-REAL 2 means
:: JGRAPH_4:def 3

  for q being Point of TOP-REAL 2 holds it.q=FanW(s,q);
end;

theorem :: JGRAPH_4:16
  for sn being Real holds (q`2/|.q.|>=sn & q`1<0 implies sn
-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)), |.q.|* ((q`2/|.q.|
  -sn)/(1-sn))]|) & (q`1>=0 implies sn-FanMorphW.q=q);

theorem :: JGRAPH_4:17
  for sn being Real st q`2/|.q.|<=sn & q`1<0 holds sn-FanMorphW.q=
|[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)), |.q.|*((q`2/|.q.|-sn)/(1+sn))]|;

theorem :: JGRAPH_4:18
  for sn being Real st -1<sn & sn<1 holds (q`2/|.q.|>=sn & q`1<=0
& q<>0.TOP-REAL 2 implies sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1-
  sn))^2)), |.q.|* ((q`2/|.q.|-sn)/(1-sn))]|) & (q`2/|.q.|<=sn & q`1<=0 & q<>0.
TOP-REAL 2 implies sn-FanMorphW.q= |[ |.q.|*(-sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)
  ), |.q.|*((q`2/|.q.|-sn)/(1+sn))]|);

theorem :: JGRAPH_4:19
  for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st sn<1 & (for p being Point of (TOP-REAL
2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1-
sn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1
  holds q`1<=0 & q<>0.TOP-REAL 2) holds f is continuous;

theorem :: JGRAPH_4:20
  for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
  being Function of (TOP-REAL 2)|K1,R^1 st -1<sn & (for p being Point of (
TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`2/|.p.|
  -sn)/(1+sn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (
  TOP-REAL 2)|K1 holds q`1<=0 & q<>0.TOP-REAL 2) holds f is continuous;

theorem :: JGRAPH_4:21
  for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st sn<1 & (for p being Point of (TOP-REAL
2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*(-sqrt(1-((p`2/|.p.|-
  sn)/(1-sn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (
  TOP-REAL 2)|K1 holds q`1<=0 & q`2/|.q.|>=sn & q<>0.TOP-REAL 2) holds f is
  continuous;

theorem :: JGRAPH_4:22
  for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
  being Function of (TOP-REAL 2)|K1,R^1 st -1<sn & (for p being Point of (
TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*(-sqrt(1-((p
  `2/|.p.|-sn)/(1+sn))^2))) & (for q being Point of TOP-REAL 2 st q in the
  carrier of (TOP-REAL 2)|K1 holds q`1<=0 & q`2/|.q.|<=sn & q<>0.TOP-REAL 2)
  holds f is continuous;

theorem :: JGRAPH_4:23
  for sn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphW)|
K0 & B0={q where q is Point of TOP-REAL 2: q`1<=0 & q<>0.TOP-REAL 2} & K0={p: p
  `2/|.p.|>=sn & p`1<=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:24
  for sn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphW)|
K0 & B0={q where q is Point of TOP-REAL 2: q`1<=0 & q<>0.TOP-REAL 2} & K0={p: p
  `2/|.p.|<=sn & p`1<=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:25
  for sn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`2
  >=sn*(|.p.|) & p`1<=0} holds K03 is closed;

theorem :: JGRAPH_4:26
  for sn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`2
  <=(sn)*(|.p.|) & p`1<=0} holds K03 is closed;

theorem :: JGRAPH_4:27
  for sn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphW)|
  K0 & B0=NonZero TOP-REAL 2 & K0={p: p`1<=0 & p<>0.TOP-REAL 2} holds f is
  continuous;

theorem :: JGRAPH_4:28
  for sn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphW)|
  K0 & B0=NonZero TOP-REAL 2 & K0={p: p`1>=0 & p<>0.TOP-REAL 2} holds f is
  continuous;

theorem :: JGRAPH_4:29
  for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL
  2)|B0 st B0=NonZero TOP-REAL 2 & K0={p: p`1<=0 & p<>0.TOP-REAL 2} holds K0 is
  closed;

theorem :: JGRAPH_4:30
  for sn being Real, B0 being Subset of TOP-REAL 2, K0 being
Subset of (TOP-REAL 2)|B0, f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL
2)|B0) st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 & B0=NonZero TOP-REAL 2 & K0={p: p
  `1<=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:31
  for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL
  2)|B0 st B0=NonZero TOP-REAL 2 & K0={p: p`1>=0 & p<>0.TOP-REAL 2} holds K0 is
  closed;

theorem :: JGRAPH_4:32
  for sn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset
  of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0)
st -1<sn & sn<1 & f=(sn-FanMorphW)|K0 & B0=NonZero TOP-REAL 2 & K0={p: p`1>=0 &
  p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:33
  for sn being Real,p being Point of TOP-REAL 2 holds |.(sn
  -FanMorphW).p.|=|.p.|;

theorem :: JGRAPH_4:34
  for sn being Real,x,K0 being set st -1<sn & sn<1 & x in K0 & K0=
  {p: p`1<=0 & p<>0.TOP-REAL 2} holds (sn-FanMorphW).x in K0;

theorem :: JGRAPH_4:35
  for sn being Real,x,K0 being set st -1<sn & sn<1 & x in K0 & K0=
  {p: p`1>=0 & p<>0.TOP-REAL 2} holds (sn-FanMorphW).x in K0;

scheme :: JGRAPH_4:sch 1
  InclSub { D() -> non empty Subset of TOP-REAL 2, P[set] } : { p : P[p] & p<>
  0.TOP-REAL 2 } c= the carrier of (TOP-REAL 2)|D()
provided
 D() = NonZero TOP-REAL 2;

theorem :: JGRAPH_4:36
  for sn being Real, D being non empty Subset of TOP-REAL 2 st -1<
  sn & sn<1 & D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(
  TOP-REAL 2)|D st h=(sn-FanMorphW)|D & h is continuous;

theorem :: JGRAPH_4:37
  for sn being Real st -1<sn & sn<1 holds ex h being Function of (
  TOP-REAL 2),(TOP-REAL 2) st h=(sn-FanMorphW) & h is continuous;

theorem :: JGRAPH_4:38
  for sn being Real st -1<sn & sn<1 holds sn-FanMorphW is one-to-one;

theorem :: JGRAPH_4:39
  for sn being Real st -1<sn & sn<1 holds sn-FanMorphW is Function
  of TOP-REAL 2,TOP-REAL 2 & rng (sn-FanMorphW) = the carrier of TOP-REAL 2;

theorem :: JGRAPH_4:40
  for sn being Real,p2 being Point of TOP-REAL 2 st -1<sn & sn<1
ex K being non empty compact Subset of TOP-REAL 2 st K = (sn-FanMorphW).:K & ex
  V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & (sn
  -FanMorphW).p2 in V2;

theorem :: JGRAPH_4:41
  for sn being Real st -1<sn & sn<1 ex f being Function of TOP-REAL 2,
  TOP-REAL 2 st f=(sn-FanMorphW) & f is being_homeomorphism;

theorem :: JGRAPH_4:42
  for sn being Real,q being Point of TOP-REAL 2 st sn<1 & q`1<0 &
q`2/|.q.|>=sn holds for p being Point of TOP-REAL 2 st p=(sn-FanMorphW).q holds
  p`1<0 & p`2>=0;

theorem :: JGRAPH_4:43
  for sn being Real,q being Point of TOP-REAL 2 st -1<sn & q`1<0 &
q`2/|.q.|<sn holds for p being Point of TOP-REAL 2 st p=(sn-FanMorphW).q holds
  p`1<0 & p`2<0;

theorem :: JGRAPH_4:44
  for sn being Real,q1,q2 being Point of TOP-REAL 2 st sn<1 & q1`1
<0 & q1`2/|.q1.|>=sn & q2`1<0 & q2`2/|.q2.|>=sn & q1`2/|.q1.|<q2`2/|.q2.| holds
for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphW).q1 & p2=(sn-FanMorphW)
  .q2 holds p1`2/|.p1.|<p2`2/|.p2.|;

theorem :: JGRAPH_4:45
  for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & q1
`1<0 & q1`2/|.q1.|<sn & q2`1<0 & q2`2/|.q2.|<sn & q1`2/|.q1.|<q2`2/|.q2.| holds
for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphW).q1 & p2=(sn-FanMorphW)
  .q2 holds p1`2/|.p1.|<p2`2/|.p2.|;

theorem :: JGRAPH_4:46
  for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1
  `1 < 0 & q2`1<0 & q1`2/|.q1.|<q2`2/|.q2.| holds for p1,p2 being Point of
TOP-REAL 2 st p1=(sn-FanMorphW).q1 & p2=(sn-FanMorphW).q2 holds p1`2/|.p1.|<p2
  `2/|.p2.|;

theorem :: JGRAPH_4:47
  for sn being Real,q being Point of TOP-REAL 2 st q`1<0 & q`2/|.q.|=sn
holds for p being Point of TOP-REAL 2 st p=(sn-FanMorphW).q holds p`1<0 & p`2=0
;

theorem :: JGRAPH_4:48
  for sn being Real holds 0.TOP-REAL 2=(sn-FanMorphW).(0.TOP-REAL
  2);

begin :: Fan Morphism for North

definition
  let s be Real, q be Point of TOP-REAL 2;
  func FanN(s,q) -> Point of TOP-REAL 2 equals
:: JGRAPH_4:def 4

  |.q.|*|[(q`1/|.q.|-s)/(1
-s), sqrt(1-((q`1/|.q.|-s)/(1-s))^2)]| if q`1/|.q.|>=s & q`2>0, |.q.|*|[(q`1/|.
  q.|-s)/(1+s), sqrt(1-((q`1/|.q.|-s)/(1+s))^2)]| if q`1/|.q.|<s & q`2>0
  otherwise q;
end;

definition
  let c be Real;
  func c-FanMorphN -> Function of TOP-REAL 2, TOP-REAL 2 means
:: JGRAPH_4:def 5

  for q being Point of TOP-REAL 2 holds it.q=FanN(c,q);
end;

theorem :: JGRAPH_4:49
  for cn being Real holds (q`1/|.q.|>=cn & q`2>0 implies cn
-FanMorphN.q= |[ |.q.|* ((q`1/|.q.|-cn)/(1-cn)), |.q.|*(sqrt(1-((q`1/|.q.|-cn)/
  (1-cn))^2))]|)& (q`2<=0 implies cn-FanMorphN.q=q);

theorem :: JGRAPH_4:50
  for cn being Real holds (q`1/|.q.|<=cn & q`2>0 implies cn
-FanMorphN.q= |[ |.q.|*((q`1/|.q.|-cn)/(1+cn)), |.q.|*( sqrt(1-((q`1/|.q.|-cn)/
  (1+cn))^2))]|);

theorem :: JGRAPH_4:51
  for cn being Real st -1<cn & cn<1 holds (q`1/|.q.|>=cn & q`2>=0
& q<>0.TOP-REAL 2 implies cn-FanMorphN.q= |[ |.q.|*((q`1/|.q.|-cn)/(1-cn)), |.q
  .|*( sqrt(1-((q`1/|.q.|-cn)/(1-cn))^2))]|) & (q`1/|.q.|<=cn & q`2>=0 & q<>0.
  TOP-REAL 2 implies cn-FanMorphN.q= |[ |.q.|*((q`1/|.q.|-cn)/(1+cn)), |.q.|*(
  sqrt(1-((q`1/|.q.|-cn)/(1+cn))^2))]|);

theorem :: JGRAPH_4:52
  for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st cn<1 & (for p being Point of (TOP-REAL
2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`1/|.p.|-cn)/(1-
cn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1
  holds q`2>=0 & q<>0.TOP-REAL 2) holds f is continuous;

theorem :: JGRAPH_4:53
  for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
  being Function of (TOP-REAL 2)|K1,R^1 st -1<cn & (for p being Point of (
TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`1/|.p.|
  -cn)/(1+cn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (
  TOP-REAL 2)|K1 holds q`2>=0 & q<>0.TOP-REAL 2) holds f is continuous;

theorem :: JGRAPH_4:54
  for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st cn<1 & (for p being Point of (TOP-REAL
2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*( sqrt(1-((p`1/|.p.|-
  cn)/(1-cn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (
  TOP-REAL 2)|K1 holds q`2>=0 & q`1/|.q.|>=cn & q<>0.TOP-REAL 2) holds f is
  continuous;

theorem :: JGRAPH_4:55
  for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
  being Function of (TOP-REAL 2)|K1,R^1 st -1<cn & (for p being Point of (
TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*( sqrt(1-((p
  `1/|.p.|-cn)/(1+cn))^2))) & (for q being Point of TOP-REAL 2 st q in the
  carrier of (TOP-REAL 2)|K1 holds q`2>=0 & q`1/|.q.|<=cn & q<>0.TOP-REAL 2)
  holds f is continuous;

theorem :: JGRAPH_4:56
  for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphN)|
K0 & B0={q where q is Point of TOP-REAL 2: q`2>=0 & q<>0.TOP-REAL 2} & K0={p: p
  `1/|.p.|>=cn & p`2>=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:57
  for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphN)|
K0 & B0={q where q is Point of TOP-REAL 2: q`2>=0 & q<>0.TOP-REAL 2} & K0={p: p
  `1/|.p.|<=cn & p`2>=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:58
  for cn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`1
  >=(cn)*(|.p.|) & p`2>=0} holds K03 is closed;

theorem :: JGRAPH_4:59
  for cn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`1
  <=(cn)*(|.p.|) & p`2>=0} holds K03 is closed;

theorem :: JGRAPH_4:60
  for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphN)|
  K0 & B0=NonZero TOP-REAL 2 & K0={p: p`2>=0 & p<>0.TOP-REAL 2} holds f is
  continuous;

theorem :: JGRAPH_4:61
  for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphN)|
  K0 & B0=NonZero TOP-REAL 2 & K0={p: p`2<=0 & p<>0.TOP-REAL 2} holds f is
  continuous;

theorem :: JGRAPH_4:62
  for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL
  2)|B0 st B0=NonZero TOP-REAL 2 & K0={p: p`2>=0 & p<>0.TOP-REAL 2} holds K0 is
  closed;

theorem :: JGRAPH_4:63
  for B0 being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL
  2)|B0 st B0=NonZero TOP-REAL 2 & K0={p: p`2<=0 & p<>0.TOP-REAL 2} holds K0 is
  closed;

theorem :: JGRAPH_4:64
  for cn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset
  of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0)
st -1<cn & cn<1 & f=(cn-FanMorphN)|K0 & B0=NonZero TOP-REAL 2 & K0={p: p`2>=0 &
  p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:65
  for cn being Real, B0 being Subset of TOP-REAL 2,K0 being Subset
  of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0)
st -1<cn & cn<1 & f=(cn-FanMorphN)|K0 & B0=NonZero TOP-REAL 2 & K0={p: p`2<=0 &
  p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:66
  for cn being Real,p being Point of TOP-REAL 2 holds |.(cn
  -FanMorphN).p.|=|.p.|;

theorem :: JGRAPH_4:67
  for cn being Real,x,K0 being set st -1<cn & cn<1 & x in K0 & K0=
  {p: p`2>=0 & p<>0.TOP-REAL 2} holds (cn-FanMorphN).x in K0;

theorem :: JGRAPH_4:68
  for cn being Real,x,K0 being set st -1<cn & cn<1 & x in K0 & K0=
  {p: p`2<=0 & p<>0.TOP-REAL 2} holds (cn-FanMorphN).x in K0;

theorem :: JGRAPH_4:69
  for cn being Real, D being non empty Subset of TOP-REAL 2 st -1<
  cn & cn<1 & D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(
  TOP-REAL 2)|D st h=(cn-FanMorphN)|D & h is continuous;

theorem :: JGRAPH_4:70
  for cn being Real st -1<cn & cn<1 holds ex h being Function of (
  TOP-REAL 2),(TOP-REAL 2) st h=(cn-FanMorphN) & h is continuous;

theorem :: JGRAPH_4:71
  for cn being Real st -1<cn & cn<1 holds cn-FanMorphN is one-to-one;

theorem :: JGRAPH_4:72
  for cn being Real st -1<cn & cn<1 holds (cn-FanMorphN) is
  Function of TOP-REAL 2,TOP-REAL 2 & rng (cn-FanMorphN) = the carrier of
  TOP-REAL 2;

theorem :: JGRAPH_4:73
  for cn being Real,p2 being Point of TOP-REAL 2 st -1<cn & cn<1
ex K being non empty compact Subset of TOP-REAL 2 st K = (cn-FanMorphN).:K & ex
  V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & (cn
  -FanMorphN).p2 in V2;

theorem :: JGRAPH_4:74
  for cn being Real st -1<cn & cn<1 ex f being Function of TOP-REAL 2,
  TOP-REAL 2 st f=cn-FanMorphN & f is being_homeomorphism;

theorem :: JGRAPH_4:75
  for cn being Real,q being Point of TOP-REAL 2 st cn<1 & q`2>0 &
q`1/|.q.|>=cn holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds
  p`2>0 & p`1>=0;

theorem :: JGRAPH_4:76
  for cn being Real,q being Point of TOP-REAL 2 st -1<cn & q`2>0 &
q`1/|.q.|<cn holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds
  p`2>0 & p`1<0;

theorem :: JGRAPH_4:77
  for cn being Real,q1,q2 being Point of TOP-REAL 2 st cn<1 & q1`2
>0 & q1`1/|.q1.|>=cn & q2`2>0 & q2`1/|.q2.|>=cn & q1`1/|.q1.|<q2`1/|.q2.| holds
for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN)
  .q2 holds p1`1/|.p1.|<p2`1/|.p2.|;

theorem :: JGRAPH_4:78
  for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & q1
`2>0 & q1`1/|.q1.|<cn & q2`2>0 & q2`1/|.q2.|<cn & q1`1/|.q1.|<q2`1/|.q2.| holds
for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN)
  .q2 holds p1`1/|.p1.|<p2`1/|.p2.|;

theorem :: JGRAPH_4:79
  for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1
  `2 > 0 & q2`2>0 & q1`1/|.q1.|<q2`1/|.q2.| holds for p1,p2 being Point of
TOP-REAL 2 st p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2 holds p1`1/|.p1.|<p2
  `1/|.p2.|;

theorem :: JGRAPH_4:80
  for cn being Real,q being Point of TOP-REAL 2 st q`2>0 & q`1/|.q.|=cn
holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds p`2>0 & p`1=0
;

theorem :: JGRAPH_4:81
  for cn being Real holds 0.TOP-REAL 2=(cn-FanMorphN).(0.TOP-REAL
  2);

begin :: Fan Morphism for East

definition
  let s be Real, q be Point of TOP-REAL 2;
  func FanE(s,q) -> Point of TOP-REAL 2 equals
:: JGRAPH_4:def 6

  |.q.|*|[sqrt(1-((q`2/|.q
.|-s)/(1-s))^2), (q`2/|.q.|-s)/(1-s)]| if q`2/|.q.|>=s & q`1>0, |.q.|*|[sqrt(1-
  ((q`2/|.q.|-s)/(1+s))^2), (q`2/|.q.|-s)/(1+s)]| if q`2/|.q.|<s & q`1>0
  otherwise q;
end;

definition
  let s be Real;
  func s-FanMorphE -> Function of TOP-REAL 2, TOP-REAL 2 means
:: JGRAPH_4:def 7

  for q being Point of TOP-REAL 2 holds it.q=FanE(s,q);
end;

theorem :: JGRAPH_4:82
  for sn being Real holds (q`2/|.q.|>=sn & q`1>0 implies sn
-FanMorphE.q= |[ |.q.|*(sqrt(1-((q`2/|.q.|-sn)/(1-sn))^2)), |.q.|* ((q`2/|.q.|-
  sn)/(1-sn))]|)& (q`1<=0 implies sn-FanMorphE.q=q);

theorem :: JGRAPH_4:83
  for sn being Real holds (q`2/|.q.|<=sn & q`1>0 implies sn
-FanMorphE.q= |[ |.q.|*(sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)), |.q.|*((q`2/|.q.|-
  sn)/(1+sn))]|);

theorem :: JGRAPH_4:84
  for sn being Real st -1<sn & sn<1 holds (q`2/|.q.|>=sn & q`1>=0
& q<>0.TOP-REAL 2 implies sn-FanMorphE.q = |[ |.q.|*(sqrt(1-((q`2/|.q.|-sn)/(1-
  sn))^2)), |.q.|* ((q`2/|.q.|-sn)/(1-sn))]|) & (q`2/|.q.|<=sn & q`1>=0 & q<>0.
TOP-REAL 2 implies sn-FanMorphE.q = |[ |.q.|*(sqrt(1-((q`2/|.q.|-sn)/(1+sn))^2)
  ), |.q.|*((q`2/|.q.|-sn)/(1+sn))]|);

theorem :: JGRAPH_4:85
  for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st sn<1 & (for p being Point of (TOP-REAL
2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`2/|.p.|-sn)/(1-
sn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1
  holds q`1>=0 & q<>0.TOP-REAL 2) holds f is continuous;

theorem :: JGRAPH_4:86
  for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
  being Function of (TOP-REAL 2)|K1,R^1 st -1<sn & (for p being Point of (
TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`2/|.p.|
  -sn)/(1+sn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (
  TOP-REAL 2)|K1 holds q`1>=0 & q<>0.TOP-REAL 2) holds f is continuous;

theorem :: JGRAPH_4:87
  for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st sn<1 & (for p being Point of (TOP-REAL
2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*(sqrt(1-((p`2/|.p.|-
  sn)/(1-sn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (
  TOP-REAL 2)|K1 holds q`1>=0 & q`2/|.q.|>=sn & q<>0.TOP-REAL 2) holds f is
  continuous;

theorem :: JGRAPH_4:88
  for sn being Real,K1 being non empty Subset of TOP-REAL 2, f
  being Function of (TOP-REAL 2)|K1,R^1 st -1<sn & (for p being Point of (
TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*(sqrt(1-((p
  `2/|.p.|-sn)/(1+sn))^2))) & (for q being Point of TOP-REAL 2 st q in the
  carrier of (TOP-REAL 2)|K1 holds q`1>=0 & q`2/|.q.|<=sn & q<>0.TOP-REAL 2)
  holds f is continuous;

theorem :: JGRAPH_4:89
  for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphE)|
K0 & B0={q where q is Point of TOP-REAL 2: q`1>=0 & q<>0.TOP-REAL 2} & K0={p: p
  `2/|.p.|>=sn & p`1>=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:90
  for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphE)|
K0 & B0={q where q is Point of TOP-REAL 2: q`1>=0 & q<>0.TOP-REAL 2} & K0={p: p
  `2/|.p.|<=sn & p`1>=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:91
  for sn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`2
  >=(sn)*(|.p.|) & p`1>=0} holds K03 is closed;

theorem :: JGRAPH_4:92
  for sn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p`2
  <=(sn)*(|.p.|) & p`1>=0} holds K03 is closed;

theorem :: JGRAPH_4:93
  for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphE)|
  K0 & B0=NonZero TOP-REAL 2 & K0={p: p`1>=0 & p<>0.TOP-REAL 2} holds f is
  continuous;

theorem :: JGRAPH_4:94
  for sn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<sn & sn<1 & f=(sn-FanMorphE)|
  K0 & B0=NonZero TOP-REAL 2 & K0={p: p`1<=0 & p<>0.TOP-REAL 2} holds f is
  continuous;

theorem :: JGRAPH_4:95
  for sn being Real, B0 being Subset of TOP-REAL 2,K0 being
Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2
)|B0) st -1<sn & sn<1 & f=(sn-FanMorphE)|K0 & B0=NonZero TOP-REAL 2 & K0={p: p
  `1>=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:96
  for sn being Real, B0 being Subset of TOP-REAL 2,K0 being
Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2
)|B0) st -1<sn & sn<1 & f=(sn-FanMorphE)|K0 & B0=NonZero TOP-REAL 2 & K0={p: p
  `1<=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:97
  for sn being Real,p being Point of TOP-REAL 2 holds |.(sn
  -FanMorphE).p.|=|.p.|;

theorem :: JGRAPH_4:98
  for sn being Real,x,K0 being set st -1<sn & sn<1 & x in K0 & K0
  ={p: p`1>=0 & p<>0.TOP-REAL 2} holds (sn-FanMorphE).x in K0;

theorem :: JGRAPH_4:99
  for sn being Real,x,K0 being set st -1<sn & sn<1 & x in K0 & K0
  ={p: p`1<=0 & p<>0.TOP-REAL 2} holds (sn-FanMorphE).x in K0;

theorem :: JGRAPH_4:100
  for sn being Real, D being non empty Subset of TOP-REAL 2 st -1
  <sn & sn<1 & D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(
  TOP-REAL 2)|D st h=(sn-FanMorphE)|D & h is continuous;

theorem :: JGRAPH_4:101
  for sn being Real st -1<sn & sn<1 holds ex h being Function of
  (TOP-REAL 2),(TOP-REAL 2) st h=(sn-FanMorphE) & h is continuous;

theorem :: JGRAPH_4:102
  for sn being Real st -1<sn & sn<1 holds sn-FanMorphE is one-to-one;

theorem :: JGRAPH_4:103
  for sn being Real st -1<sn & sn<1 holds (sn-FanMorphE) is
  Function of TOP-REAL 2,TOP-REAL 2 & rng (sn-FanMorphE) = the carrier of
  TOP-REAL 2;

theorem :: JGRAPH_4:104
  for sn being Real,p2 being Point of TOP-REAL 2 st -1<sn & sn<1
ex K being non empty compact Subset of TOP-REAL 2 st K = (sn-FanMorphE).:K & ex
  V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & (sn
  -FanMorphE).p2 in V2;

theorem :: JGRAPH_4:105
  for sn being Real st -1<sn & sn<1 ex f being Function of TOP-REAL 2,
  TOP-REAL 2 st f=(sn-FanMorphE) & f is being_homeomorphism;

theorem :: JGRAPH_4:106
  for sn being Real,q being Point of TOP-REAL 2 st sn<1 & q`1>0 &
q`2/|.q.|>=sn holds for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q holds
  p`1>0 & p`2>=0;

theorem :: JGRAPH_4:107
  for sn being Real,q being Point of TOP-REAL 2 st -1<sn & q`1>0
  & q`2/|.q.|<sn holds for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q
  holds p`1>0 & p`2<0;

theorem :: JGRAPH_4:108
  for sn being Real,q1,q2 being Point of TOP-REAL 2 st sn<1 & q1
  `1>0 & q1`2/|.q1.|>=sn & q2`1>0 & q2`2/|.q2.|>=sn & q1`2/|.q1.|<q2`2/|.q2.|
  holds for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphE).q1 & p2=(sn
  -FanMorphE).q2 holds p1`2/|.p1.|<p2`2/|.p2.|;

theorem :: JGRAPH_4:109
  for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & q1
`1>0 & q1`2/|.q1.|<sn & q2`1>0 & q2`2/|.q2.|<sn & q1`2/|.q1.|<q2`2/|.q2.| holds
for p1,p2 being Point of TOP-REAL 2 st p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE)
  .q2 holds p1`2/|.p1.|<p2`2/|.p2.|;

theorem :: JGRAPH_4:110
  for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1
`1>0 & q2`1>0 & q1`2/|.q1.|<q2`2/|.q2.| holds for p1,p2 being Point of TOP-REAL
2 st p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2 holds p1`2/|.p1.|<p2`2/|.p2.|;

theorem :: JGRAPH_4:111
  for sn being Real,q being Point of TOP-REAL 2 st q`1>0 & q`2/|.q.|=sn
holds for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q holds p`1>0 & p`2=0
;

theorem :: JGRAPH_4:112
  for sn being Real holds 0.TOP-REAL 2=(sn-FanMorphE).(0.TOP-REAL
  2);

begin :: Fan Morphism for South

definition
  let s be Real, q be Point of TOP-REAL 2;
  func FanS(s,q) -> Point of TOP-REAL 2 equals
:: JGRAPH_4:def 8

  |.q.|*|[(q`1/|.q.|-s)/(1
-s), -sqrt(1-((q`1/|.q.|-s)/(1-s))^2)]| if q`1/|.q.|>=s & q`2<0, |.q.|*|[(q`1/
  |.q.|-s)/(1+s), -sqrt(1-((q`1/|.q.|-s)/(1+s))^2)]| if q`1/|.q.|<s & q`2<0
  otherwise q;
end;

definition
  let c be Real;
  func c-FanMorphS -> Function of TOP-REAL 2, TOP-REAL 2 means
:: JGRAPH_4:def 9

  for q being Point of TOP-REAL 2 holds it.q=FanS(c,q);
end;

theorem :: JGRAPH_4:113
  for cn being Real holds (q`1/|.q.|>=cn & q`2<0 implies
cn-FanMorphS.q= |[ |.q.|* ((q`1/|.q.|-cn)/(1-cn)), |.q.|*(-sqrt(1-((q`1/|.q.|-
  cn)/(1-cn))^2))]|)& (q`2>=0 implies cn-FanMorphS.q=q);

theorem :: JGRAPH_4:114
  for cn being Real holds (q`1/|.q.|<=cn & q`2<0 implies cn
-FanMorphS.q= |[ |.q.|*((q`1/|.q.|-cn)/(1+cn)), |.q.|*( -sqrt(1-((q`1/|.q.|-cn)
  /(1+cn))^2))]|);

theorem :: JGRAPH_4:115
  for cn being Real st -1<cn & cn<1 holds (q`1/|.q.|>=cn & q`2<=0
  & q<>0.TOP-REAL 2 implies cn-FanMorphS.q = |[ |.q.|* ((q`1/|.q.|-cn)/(1-cn)),
|.q.|*( -sqrt(1-((q`1/|.q.|-cn)/(1-cn))^2))]|) & (q`1/|.q.|<=cn & q`2<=0 & q<>
0.TOP-REAL 2 implies cn-FanMorphS.q = |[ |.q.|*((q`1/|.q.|-cn)/(1+cn)), |.q.|*(
  -sqrt(1-((q`1/|.q.|-cn)/(1+cn))^2))]|);

theorem :: JGRAPH_4:116
  for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st cn<1 & (for p being Point of (TOP-REAL
2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`1/|.p.|-cn)/(1-
cn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1
  holds q`2<=0 & q<>0.TOP-REAL 2) holds f is continuous;

theorem :: JGRAPH_4:117
  for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
  being Function of (TOP-REAL 2)|K1,R^1 st -1<cn & (for p being Point of (
TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|* ((p`1/|.p.|
  -cn)/(1+cn))) & (for q being Point of TOP-REAL 2 st q in the carrier of (
  TOP-REAL 2)|K1 holds q`2<=0 & q<>0.TOP-REAL 2) holds f is continuous;

theorem :: JGRAPH_4:118
  for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
being Function of (TOP-REAL 2)|K1,R^1 st cn<1 & (for p being Point of (TOP-REAL
2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*( -sqrt(1-((p`1/|.p.|
  -cn)/(1-cn))^2))) & (for q being Point of TOP-REAL 2 st q in the carrier of (
  TOP-REAL 2)|K1 holds q`2<=0 & q`1/|.q.|>=cn & q<>0.TOP-REAL 2) holds f is
  continuous;

theorem :: JGRAPH_4:119
  for cn being Real,K1 being non empty Subset of TOP-REAL 2, f
  being Function of (TOP-REAL 2)|K1,R^1 st -1<cn & (for p being Point of (
TOP-REAL 2) st p in the carrier of (TOP-REAL 2)|K1 holds f.p=|.p.|*( -sqrt(1-((
  p`1/|.p.|-cn)/(1+cn))^2))) & (for q being Point of TOP-REAL 2 st q in the
  carrier of (TOP-REAL 2)|K1 holds q`2<=0 & q`1/|.q.|<=cn & q<>0.TOP-REAL 2)
  holds f is continuous;

theorem :: JGRAPH_4:120
  for cn being Real, K0,B0 being Subset of TOP-REAL 2,f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphS)|
K0 & B0={q where q is Point of TOP-REAL 2: q`2<=0 & q<>0.TOP-REAL 2} & K0={p: p
  `1/|.p.|>=cn & p`2<=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:121
  for cn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphS)|
K0 & B0={q where q is Point of TOP-REAL 2: q`2<=0 & q<>0.TOP-REAL 2} & K0={p: p
  `1/|.p.|<=cn & p`2<=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:122
  for cn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p
  `1>=(cn)*(|.p.|) & p`2<=0} holds K03 is closed;

theorem :: JGRAPH_4:123
  for cn being Real, K03 being Subset of TOP-REAL 2 st K03={p: p
  `1<=(cn)*(|.p.|) & p`2<=0} holds K03 is closed;

theorem :: JGRAPH_4:124
  for cn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphS)|
  K0 & B0=NonZero TOP-REAL 2 & K0={p: p`2<=0 & p<>0.TOP-REAL 2} holds f is
  continuous;

theorem :: JGRAPH_4:125
  for cn being Real, K0,B0 being Subset of TOP-REAL 2, f being
Function of (TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st -1<cn & cn<1 & f=(cn-FanMorphS)|
  K0 & B0=NonZero TOP-REAL 2 & K0={p: p`2>=0 & p<>0.TOP-REAL 2} holds f is
  continuous;

theorem :: JGRAPH_4:126
  for cn being Real, B0 being Subset of TOP-REAL 2,K0 being
Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2
)|B0) st -1<cn & cn<1 & f=(cn-FanMorphS)|K0 & B0=NonZero TOP-REAL 2 & K0={p: p
  `2<=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:127
  for cn being Real, B0 being Subset of TOP-REAL 2,K0 being
Subset of (TOP-REAL 2)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2
)|B0) st -1<cn & cn<1 & f=(cn-FanMorphS)|K0 & B0=NonZero TOP-REAL 2 & K0={p: p
  `2>=0 & p<>0.TOP-REAL 2} holds f is continuous;

theorem :: JGRAPH_4:128
  for cn being Real,p being Point of TOP-REAL 2 holds |.(cn
  -FanMorphS).p.|=|.p.|;

theorem :: JGRAPH_4:129
  for cn being Real,x,K0 being set st -1<cn & cn<1 & x in K0 & K0
  ={p: p`2<=0 & p<>0.TOP-REAL 2} holds (cn-FanMorphS).x in K0;

theorem :: JGRAPH_4:130
  for cn being Real,x,K0 being set st -1<cn & cn<1 & x in K0 & K0
  ={p: p`2>=0 & p<>0.TOP-REAL 2} holds (cn-FanMorphS).x in K0;

theorem :: JGRAPH_4:131
  for cn being Real, D being non empty Subset of TOP-REAL 2 st -1
  <cn & cn<1 & D`={0.TOP-REAL 2} holds ex h being Function of (TOP-REAL 2)|D,(
  TOP-REAL 2)|D st h=(cn-FanMorphS)|D & h is continuous;

theorem :: JGRAPH_4:132
  for cn being Real st -1<cn & cn<1 holds cn-FanMorphS is continuous;

theorem :: JGRAPH_4:133
  for cn being Real st -1<cn & cn<1 holds cn-FanMorphS is one-to-one;

theorem :: JGRAPH_4:134
  for cn being Real st -1<cn & cn<1 holds (cn-FanMorphS) is
  Function of TOP-REAL 2,TOP-REAL 2 & rng (cn-FanMorphS) = the carrier of
  TOP-REAL 2;

theorem :: JGRAPH_4:135
  for cn being Real,p2 being Point of TOP-REAL 2 st -1<cn & cn<1
ex K being non empty compact Subset of TOP-REAL 2 st K = (cn-FanMorphS).:K & ex
  V2 being Subset of TOP-REAL 2 st p2 in V2 & V2 is open & V2 c= K & (cn
  -FanMorphS).p2 in V2;

theorem :: JGRAPH_4:136
  for cn being Real st -1<cn & cn<1 ex f being Function of TOP-REAL 2,
  TOP-REAL 2 st f=cn-FanMorphS & f is being_homeomorphism;

theorem :: JGRAPH_4:137
  for cn being Real,q being Point of TOP-REAL 2 st cn<1 & q`2<0 &
q`1/|.q.|>=cn holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphS).q holds
  p`2<0 & p`1>=0;

theorem :: JGRAPH_4:138
  for cn being Real,q being Point of TOP-REAL 2 st -1<cn & q`2<0
  & q`1/|.q.|<cn holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphS).q
  holds p`2<0 & p`1<0;

theorem :: JGRAPH_4:139
  for cn being Real,q1,q2 being Point of TOP-REAL 2 st cn<1 & q1
  `2<0 & q1`1/|.q1.|>=cn & q2`2<0 & q2`1/|.q2.|>=cn & q1`1/|.q1.|<q2`1/|.q2.|
  holds for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphS).q1 & p2=(cn
  -FanMorphS).q2 holds p1`1/|.p1.|<p2`1/|.p2.|;

theorem :: JGRAPH_4:140
  for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & q1
`2<0 & q1`1/|.q1.|<cn & q2`2<0 & q2`1/|.q2.|<cn & q1`1/|.q1.|<q2`1/|.q2.| holds
for p1,p2 being Point of TOP-REAL 2 st p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS)
  .q2 holds p1`1/|.p1.|<p2`1/|.p2.|;

theorem :: JGRAPH_4:141
  for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1
`2<0 & q2`2<0 & q1`1/|.q1.|<q2`1/|.q2.| holds for p1,p2 being Point of TOP-REAL
2 st p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2 holds p1`1/|.p1.|<p2`1/|.p2.|;

theorem :: JGRAPH_4:142
  for cn being Real,q being Point of TOP-REAL 2 st q`2<0 & q`1/|.q.|=cn
holds for p being Point of TOP-REAL 2 st p=(cn-FanMorphS).q holds p`2<0 & p`1=0
;

theorem :: JGRAPH_4:143
  0.TOP-REAL 2 = (a-FanMorphS).(0.TOP-REAL 2);