:: Fan Homeomorphisms in the Plane
:: by Yatsuka Nakamura
::
:: Copyright (c) 2002-2021 Association of Mizar Users

Lm1: for p being Point of () st p <> 0. () holds
|.p.| > 0

proof end;

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

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

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

theorem Th4: :: JGRAPH_4:4
for X being non empty TopSpace
for f1, f2 being Function of X,R^1
for 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
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = ((r1 / r2) - a) / b ) & g is continuous )
proof end;

theorem Th5: :: JGRAPH_4:5
for X being non empty TopSpace
for f1, f2 being Function of X,R^1
for 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
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r2 * (((r1 / r2) - a) / b) ) & g is continuous )
proof end;

theorem Th6: :: JGRAPH_4:6
for X being non empty TopSpace
for 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
for r1 being Real st f1 . p = r1 holds
g . p = r1 ^2 ) & g is continuous )
proof end;

theorem Th7: :: JGRAPH_4:7
for X being non empty TopSpace
for 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
for r1 being Real st f1 . p = r1 holds
g . p = |.r1.| ) & g is continuous )
proof end;

theorem Th8: :: JGRAPH_4:8
for X being non empty TopSpace
for 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
for r1 being Real st f1 . p = r1 holds
g . p = - r1 ) & g is continuous )
proof end;

theorem Th9: :: JGRAPH_4:9
for X being non empty TopSpace
for f1, f2 being Function of X,R^1
for 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
for 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 )
proof end;

theorem Th10: :: JGRAPH_4:10
for X being non empty TopSpace
for f1, f2 being Function of X,R^1
for 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
for 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 )
proof end;

definition
let n be Nat;
deffunc H1( Point of ()) -> object = |.\$1.|;
func n NormF -> Function of (),R^1 means :Def1: :: JGRAPH_4:def 1
for q being Point of () holds it . q = |.q.|;
existence
ex b1 being Function of (),R^1 st
for q being Point of () holds b1 . q = |.q.|
proof end;
uniqueness
for b1, b2 being Function of (),R^1 st ( for q being Point of () holds b1 . q = |.q.| ) & ( for q being Point of () holds b2 . q = |.q.| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines NormF JGRAPH_4:def 1 :
for n being Nat
for b2 being Function of (),R^1 holds
( b2 = n NormF iff for q being Point of () holds b2 . q = |.q.| );

theorem :: JGRAPH_4:11
for n being Nat holds
( dom () = the carrier of () & dom () = REAL n )
proof end;

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

registration
let n be Nat;
coherence by Th12;
end;

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

theorem Th14: :: JGRAPH_4:14
for n being Element of NAT
for p being Point of ()
for r being Real
for B being Subset of () st B = cl_Ball (p,r) holds
( B is bounded & B is closed )
proof end;

theorem Th15: :: JGRAPH_4:15
for p being Point of ()
for r being Real
for B being Subset of () st B = cl_Ball (p,r) holds
B is compact
proof end;

definition
let s be Real;
let q be Point of ();
func FanW (s,q) -> Point of () equals :Def2: :: 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;
correctness
coherence
( ( (q 2) / |.q.| >= s & q 1 < 0 implies |.q.| * |[(- (sqrt (1 - (((((q 2) / |.q.|) - s) / (1 - s)) ^2)))),((((q 2) / |.q.|) - s) / (1 - s))]| is Point of () ) & ( (q 2) / |.q.| < s & q 1 < 0 implies |.q.| * |[(- (sqrt (1 - (((((q 2) / |.q.|) - s) / (1 + s)) ^2)))),((((q 2) / |.q.|) - s) / (1 + s))]| is Point of () ) & ( ( not (q 2) / |.q.| >= s or not q 1 < 0 ) & ( not (q 2) / |.q.| < s or not q 1 < 0 ) implies q is Point of () ) )
;
consistency
for b1 being Point of () st (q 2) / |.q.| >= s & q 1 < 0 & (q 2) / |.q.| < s & q 1 < 0 holds
( b1 = |.q.| * |[(- (sqrt (1 - (((((q 2) / |.q.|) - s) / (1 - s)) ^2)))),((((q 2) / |.q.|) - s) / (1 - s))]| iff b1 = |.q.| * |[(- (sqrt (1 - (((((q 2) / |.q.|) - s) / (1 + s)) ^2)))),((((q 2) / |.q.|) - s) / (1 + s))]| )
;
;
end;

:: deftheorem Def2 defines FanW JGRAPH_4:def 2 :
for s being Real
for q being Point of () holds
( ( (q 2) / |.q.| >= s & q 1 < 0 implies FanW (s,q) = |.q.| * |[(- (sqrt (1 - (((((q 2) / |.q.|) - s) / (1 - s)) ^2)))),((((q 2) / |.q.|) - s) / (1 - s))]| ) & ( (q 2) / |.q.| < s & q 1 < 0 implies FanW (s,q) = |.q.| * |[(- (sqrt (1 - (((((q 2) / |.q.|) - s) / (1 + s)) ^2)))),((((q 2) / |.q.|) - s) / (1 + s))]| ) & ( ( not (q 2) / |.q.| >= s or not q 1 < 0 ) & ( not (q 2) / |.q.| < s or not q 1 < 0 ) implies FanW (s,q) = q ) );

definition
let s be Real;
func s -FanMorphW -> Function of (),() means :Def3: :: JGRAPH_4:def 3
for q being Point of () holds it . q = FanW (s,q);
existence
ex b1 being Function of (),() st
for q being Point of () holds b1 . q = FanW (s,q)
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for q being Point of () holds b1 . q = FanW (s,q) ) & ( for q being Point of () holds b2 . q = FanW (s,q) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines -FanMorphW JGRAPH_4:def 3 :
for s being Real
for b2 being Function of (),() holds
( b2 = s -FanMorphW iff for q being Point of () holds b2 . q = FanW (s,q) );

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

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

theorem Th18: :: JGRAPH_4:18
for q being Point of ()
for sn being Real st - 1 < sn & sn < 1 holds
( ( (q 2) / |.q.| >= sn & q 1 <= 0 & q <> 0. () implies () . 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. () implies () . q = |[(|.q.| * (- (sqrt (1 - (((((q 2) / |.q.|) - sn) / (1 + sn)) ^2))))),(|.q.| * ((((q 2) / |.q.|) - sn) / (1 + sn)))]| ) )
proof end;

Lm2: for K being non empty Subset of () holds
( proj1 | K is continuous Function of (() | K),R^1 & ( for q being Point of (() | K) holds () . q = proj1 . q ) )

proof end;

Lm3: for K being non empty Subset of () holds
( proj2 | K is continuous Function of (() | K),R^1 & ( for q being Point of (() | K) holds () . q = proj2 . q ) )

proof end;

Lm4: dom () = the carrier of ()
by FUNCT_2:def 1;

Lm5: for K being non empty Subset of () holds
( () | K is continuous Function of (() | K),R^1 & ( for q being Point of (() | K) holds (() | K) . q = () . q ) )

proof end;

Lm6: for K1 being non empty Subset of ()
for g1 being Function of (() | K1),R^1 st g1 = () | K1 & ( for q being Point of () st q in the carrier of (() | K1) holds
q <> 0. () ) holds
for q being Point of (() | K1) holds g1 . q <> 0

proof end;

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

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

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

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

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

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

Lm7: for sn being Real
for K1 being Subset of () st K1 = { p7 where p7 is Point of () : p7 2 >= sn * |.p7.| } holds
K1 is closed

proof end;

Lm8: for sn being Real
for K1 being Subset of () st K1 = { p7 where p7 is Point of () : p7 1 >= sn * |.p7.| } holds
K1 is closed

proof end;

theorem Th25: :: JGRAPH_4:25
for sn being Real
for K03 being Subset of () st K03 = { p where p is Point of () : ( p 2 >= sn * |.p.| & p 1 <= 0 ) } holds
K03 is closed
proof end;

Lm9: for sn being Real
for K1 being Subset of () st K1 = { p7 where p7 is Point of () : p7 2 <= sn * |.p7.| } holds
K1 is closed

proof end;

Lm10: for sn being Real
for K1 being Subset of () st K1 = { p7 where p7 is Point of () : p7 1 <= sn * |.p7.| } holds
K1 is closed

proof end;

theorem Th26: :: JGRAPH_4:26
for sn being Real
for K03 being Subset of () st K03 = { p where p is Point of () : ( p 2 <= sn * |.p.| & p 1 <= 0 ) } holds
K03 is closed
proof end;

theorem Th27: :: JGRAPH_4:27
for sn being Real
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st - 1 < sn & sn < 1 & f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 <= 0 & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th28: :: JGRAPH_4:28
for sn being Real
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st - 1 < sn & sn < 1 & f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 >= 0 & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th29: :: JGRAPH_4:29
for B0 being Subset of ()
for K0 being Subset of (() | B0) st B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 <= 0 & p <> 0. () ) } holds
K0 is closed
proof end;

theorem Th30: :: JGRAPH_4:30
for sn being Real
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st - 1 < sn & sn < 1 & f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 <= 0 & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th31: :: JGRAPH_4:31
for B0 being Subset of ()
for K0 being Subset of (() | B0) st B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 >= 0 & p <> 0. () ) } holds
K0 is closed
proof end;

theorem Th32: :: JGRAPH_4:32
for sn being Real
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st - 1 < sn & sn < 1 & f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 >= 0 & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th33: :: JGRAPH_4:33
for sn being Real
for p being Point of () holds |.(() . p).| = |.p.|
proof end;

theorem Th34: :: JGRAPH_4:34
for sn being Real
for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of () : ( p 1 <= 0 & p <> 0. () ) } holds
() . x in K0
proof end;

theorem Th35: :: JGRAPH_4:35
for sn being Real
for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of () : ( p 1 >= 0 & p <> 0. () ) } holds
() . x in K0
proof end;

scheme :: JGRAPH_4:sch 1
InclSub{ F1() -> non empty Subset of (), P1[ set ] } :
{ p where p is Point of () : ( P1[p] & p <> 0. () ) } c= the carrier of (() | F1())
provided
A1: F1() = NonZero ()
proof end;

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

Lm11: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr ()
by EUCLID:def 8;

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

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

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

Lm12: for q4, q, p2 being Point of ()
for O, u, uq being Point of () st u in cl_Ball (O,(|.p2.| + 1)) & q = uq & q4 = u & O = 0. () & |.q4.| = |.q.| holds
q in cl_Ball (O,(|.p2.| + 1))

proof end;

theorem Th40: :: JGRAPH_4:40
for sn being Real
for p2 being Point of () st - 1 < sn & sn < 1 holds
ex K being non empty compact Subset of () st
( K = () .: K & ex V2 being Subset of () st
( p2 in V2 & V2 is open & V2 c= K & () . p2 in V2 ) )
proof end;

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

Lm13: now :: thesis: for q being Point of ()
for sn, t being Real st ((- ((t / |.q.|) - sn)) / (1 - sn)) ^2 < 1 ^2 holds
- (sqrt (1 - ((((t / |.q.|) - sn) / (1 - sn)) ^2))) < - 0
let q be Point of (); :: thesis: for sn, t being Real st ((- ((t / |.q.|) - sn)) / (1 - sn)) ^2 < 1 ^2 holds
- (sqrt (1 - ((((t / |.q.|) - sn) / (1 - sn)) ^2))) < - 0

let sn, t be Real; :: thesis: ( ((- ((t / |.q.|) - sn)) / (1 - sn)) ^2 < 1 ^2 implies - (sqrt (1 - ((((t / |.q.|) - sn) / (1 - sn)) ^2))) < - 0 )
assume ((- ((t / |.q.|) - sn)) / (1 - sn)) ^2 < 1 ^2 ; :: thesis: - (sqrt (1 - ((((t / |.q.|) - sn) / (1 - sn)) ^2))) < - 0
then 1 - (((- ((t / |.q.|) - sn)) / (1 - sn)) ^2) > 0 by XREAL_1:50;
then sqrt (1 - (((- ((t / |.q.|) - sn)) / (1 - sn)) ^2)) > 0 by SQUARE_1:25;
then sqrt (1 - (((- ((t / |.q.|) - sn)) ^2) / ((1 - sn) ^2))) > 0 by XCMPLX_1:76;
then sqrt (1 - ((((t / |.q.|) - sn) ^2) / ((1 - sn) ^2))) > 0 ;
then sqrt (1 - ((((t / |.q.|) - sn) / (1 - sn)) ^2)) > 0 by XCMPLX_1:76;
hence - (sqrt (1 - ((((t / |.q.|) - sn) / (1 - sn)) ^2))) < - 0 by XREAL_1:24; :: thesis: verum
end;

theorem Th42: :: JGRAPH_4:42
for sn being Real
for q being Point of () st sn < 1 & q 1 < 0 & (q 2) / |.q.| >= sn holds
for p being Point of () st p = () . q holds
( p 1 < 0 & p 2 >= 0 )
proof end;

theorem Th43: :: JGRAPH_4:43
for sn being Real
for q being Point of () st - 1 < sn & q 1 < 0 & (q 2) / |.q.| < sn holds
for p being Point of () st p = () . q holds
( p 1 < 0 & p 2 < 0 )
proof end;

theorem Th44: :: JGRAPH_4:44
for sn being Real
for q1, q2 being Point of () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 2) / |.p1.| < (p2 2) / |.p2.|
proof end;

theorem Th45: :: JGRAPH_4:45
for sn being Real
for q1, q2 being Point of () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 2) / |.p1.| < (p2 2) / |.p2.|
proof end;

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

theorem :: JGRAPH_4:47
for sn being Real
for q being Point of () st q 1 < 0 & (q 2) / |.q.| = sn holds
for p being Point of () st p = () . q holds
( p 1 < 0 & p 2 = 0 )
proof end;

theorem :: JGRAPH_4:48
for sn being Real holds 0. () = () . (0. ()) by ;

definition
let s be Real;
let q be Point of ();
func FanN (s,q) -> Point of () equals :Def4: :: 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;
correctness
coherence
( ( (q 1) / |.q.| >= s & q 2 > 0 implies |.q.| * |[((((q 1) / |.q.|) - s) / (1 - s)),(sqrt (1 - (((((q 1) / |.q.|) - s) / (1 - s)) ^2)))]| is Point of () ) & ( (q 1) / |.q.| < s & q 2 > 0 implies |.q.| * |[((((q 1) / |.q.|) - s) / (1 + s)),(sqrt (1 - (((((q 1) / |.q.|) - s) / (1 + s)) ^2)))]| is Point of () ) & ( ( not (q 1) / |.q.| >= s or not q 2 > 0 ) & ( not (q 1) / |.q.| < s or not q 2 > 0 ) implies q is Point of () ) )
;
consistency
for b1 being Point of () st (q 1) / |.q.| >= s & q 2 > 0 & (q 1) / |.q.| < s & q 2 > 0 holds
( b1 = |.q.| * |[((((q 1) / |.q.|) - s) / (1 - s)),(sqrt (1 - (((((q 1) / |.q.|) - s) / (1 - s)) ^2)))]| iff b1 = |.q.| * |[((((q 1) / |.q.|) - s) / (1 + s)),(sqrt (1 - (((((q 1) / |.q.|) - s) / (1 + s)) ^2)))]| )
;
;
end;

:: deftheorem Def4 defines FanN JGRAPH_4:def 4 :
for s being Real
for q being Point of () holds
( ( (q 1) / |.q.| >= s & q 2 > 0 implies FanN (s,q) = |.q.| * |[((((q 1) / |.q.|) - s) / (1 - s)),(sqrt (1 - (((((q 1) / |.q.|) - s) / (1 - s)) ^2)))]| ) & ( (q 1) / |.q.| < s & q 2 > 0 implies FanN (s,q) = |.q.| * |[((((q 1) / |.q.|) - s) / (1 + s)),(sqrt (1 - (((((q 1) / |.q.|) - s) / (1 + s)) ^2)))]| ) & ( ( not (q 1) / |.q.| >= s or not q 2 > 0 ) & ( not (q 1) / |.q.| < s or not q 2 > 0 ) implies FanN (s,q) = q ) );

definition
let c be Real;
func c -FanMorphN -> Function of (),() means :Def5: :: JGRAPH_4:def 5
for q being Point of () holds it . q = FanN (c,q);
existence
ex b1 being Function of (),() st
for q being Point of () holds b1 . q = FanN (c,q)
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for q being Point of () holds b1 . q = FanN (c,q) ) & ( for q being Point of () holds b2 . q = FanN (c,q) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines -FanMorphN JGRAPH_4:def 5 :
for c being Real
for b2 being Function of (),() holds
( b2 = c -FanMorphN iff for q being Point of () holds b2 . q = FanN (c,q) );

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

theorem Th50: :: JGRAPH_4:50
for q being Point of ()
for cn being Real st (q 1) / |.q.| <= cn & q 2 > 0 holds
() . q = |[(|.q.| * ((((q 1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q 1) / |.q.|) - cn) / (1 + cn)) ^2))))]|
proof end;

theorem Th51: :: JGRAPH_4:51
for q being Point of ()
for cn being Real st - 1 < cn & cn < 1 holds
( ( (q 1) / |.q.| >= cn & q 2 >= 0 & q <> 0. () implies () . 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. () implies () . q = |[(|.q.| * ((((q 1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q 1) / |.q.|) - cn) / (1 + cn)) ^2))))]| ) )
proof end;

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

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

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

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

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

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

theorem Th58: :: JGRAPH_4:58
for cn being Real
for K03 being Subset of () st K03 = { p where p is Point of () : ( p 1 >= cn * |.p.| & p 2 >= 0 ) } holds
K03 is closed
proof end;

theorem Th59: :: JGRAPH_4:59
for cn being Real
for K03 being Subset of () st K03 = { p where p is Point of () : ( p 1 <= cn * |.p.| & p 2 >= 0 ) } holds
K03 is closed
proof end;

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

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

theorem Th62: :: JGRAPH_4:62
for B0 being Subset of ()
for K0 being Subset of (() | B0) st B0 = NonZero () & K0 = { p where p is Point of () : ( p 2 >= 0 & p <> 0. () ) } holds
K0 is closed
proof end;

theorem Th63: :: JGRAPH_4:63
for B0 being Subset of ()
for K0 being Subset of (() | B0) st B0 = NonZero () & K0 = { p where p is Point of () : ( p 2 <= 0 & p <> 0. () ) } holds
K0 is closed
proof end;

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

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

theorem Th66: :: JGRAPH_4:66
for cn being Real
for p being Point of () holds |.(() . p).| = |.p.|
proof end;

theorem Th67: :: JGRAPH_4:67
for cn being Real
for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of () : ( p 2 >= 0 & p <> 0. () ) } holds
() . x in K0
proof end;

theorem Th68: :: JGRAPH_4:68
for cn being Real
for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of () : ( p 2 <= 0 & p <> 0. () ) } holds
() . x in K0
proof end;

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

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

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

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

theorem Th73: :: JGRAPH_4:73
for cn being Real
for p2 being Point of () st - 1 < cn & cn < 1 holds
ex K being non empty compact Subset of () st
( K = () .: K & ex V2 being Subset of () st
( p2 in V2 & V2 is open & V2 c= K & () . p2 in V2 ) )
proof end;

theorem :: JGRAPH_4:74
for cn being Real st - 1 < cn & cn < 1 holds
ex f being Function of (),() st
( f = cn -FanMorphN & f is being_homeomorphism )
proof end;

theorem Th75: :: JGRAPH_4:75
for cn being Real
for q being Point of () st cn < 1 & q 2 > 0 & (q 1) / |.q.| >= cn holds
for p being Point of () st p = () . q holds
( p 2 > 0 & p 1 >= 0 )
proof end;

theorem Th76: :: JGRAPH_4:76
for cn being Real
for q being Point of () st - 1 < cn & q 2 > 0 & (q 1) / |.q.| < cn holds
for p being Point of () st p = () . q holds
( p 2 > 0 & p 1 < 0 )
proof end;

theorem Th77: :: JGRAPH_4:77
for cn being Real
for q1, q2 being Point of () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 1) / |.p1.| < (p2 1) / |.p2.|
proof end;

theorem Th78: :: JGRAPH_4:78
for cn being Real
for q1, q2 being Point of () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 1) / |.p1.| < (p2 1) / |.p2.|
proof end;

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

theorem :: JGRAPH_4:80
for cn being Real
for q being Point of () st q 2 > 0 & (q 1) / |.q.| = cn holds
for p being Point of () st p = () . q holds
( p 2 > 0 & p 1 = 0 )
proof end;

theorem :: JGRAPH_4:81
for cn being Real holds 0. () = () . (0. ()) by ;

definition
let s be Real;
let q be Point of ();
func FanE (s,q) -> Point of () equals :Def6: :: 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;
correctness
coherence
( ( (q 2) / |.q.| >= s & q 1 > 0 implies |.q.| * |[(sqrt (1 - (((((q 2) / |.q.|) - s) / (1 - s)) ^2))),((((q 2) / |.q.|) - s) / (1 - s))]| is Point of () ) & ( (q 2) / |.q.| < s & q 1 > 0 implies |.q.| * |[(sqrt (1 - (((((q 2) / |.q.|) - s) / (1 + s)) ^2))),((((q 2) / |.q.|) - s) / (1 + s))]| is Point of () ) & ( ( not (q 2) / |.q.| >= s or not q 1 > 0 ) & ( not (q 2) / |.q.| < s or not q 1 > 0 ) implies q is Point of () ) )
;
consistency
for b1 being Point of () st (q 2) / |.q.| >= s & q 1 > 0 & (q 2) / |.q.| < s & q 1 > 0 holds
( b1 = |.q.| * |[(sqrt (1 - (((((q 2) / |.q.|) - s) / (1 - s)) ^2))),((((q 2) / |.q.|) - s) / (1 - s))]| iff b1 = |.q.| * |[(sqrt (1 - (((((q 2) / |.q.|) - s) / (1 + s)) ^2))),((((q 2) / |.q.|) - s) / (1 + s))]| )
;
;
end;

:: deftheorem Def6 defines FanE JGRAPH_4:def 6 :
for s being Real
for q being Point of () holds
( ( (q 2) / |.q.| >= s & q 1 > 0 implies FanE (s,q) = |.q.| * |[(sqrt (1 - (((((q 2) / |.q.|) - s) / (1 - s)) ^2))),((((q 2) / |.q.|) - s) / (1 - s))]| ) & ( (q 2) / |.q.| < s & q 1 > 0 implies FanE (s,q) = |.q.| * |[(sqrt (1 - (((((q 2) / |.q.|) - s) / (1 + s)) ^2))),((((q 2) / |.q.|) - s) / (1 + s))]| ) & ( ( not (q 2) / |.q.| >= s or not q 1 > 0 ) & ( not (q 2) / |.q.| < s or not q 1 > 0 ) implies FanE (s,q) = q ) );

definition
let s be Real;
func s -FanMorphE -> Function of (),() means :Def7: :: JGRAPH_4:def 7
for q being Point of () holds it . q = FanE (s,q);
existence
ex b1 being Function of (),() st
for q being Point of () holds b1 . q = FanE (s,q)
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for q being Point of () holds b1 . q = FanE (s,q) ) & ( for q being Point of () holds b2 . q = FanE (s,q) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines -FanMorphE JGRAPH_4:def 7 :
for s being Real
for b2 being Function of (),() holds
( b2 = s -FanMorphE iff for q being Point of () holds b2 . q = FanE (s,q) );

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

theorem Th83: :: JGRAPH_4:83
for q being Point of ()
for sn being Real st (q 2) / |.q.| <= sn & q 1 > 0 holds
() . q = |[(|.q.| * (sqrt (1 - (((((q 2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q 2) / |.q.|) - sn) / (1 + sn)))]|
proof end;

theorem Th84: :: JGRAPH_4:84
for q being Point of ()
for sn being Real st - 1 < sn & sn < 1 holds
( ( (q 2) / |.q.| >= sn & q 1 >= 0 & q <> 0. () implies () . 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. () implies () . q = |[(|.q.| * (sqrt (1 - (((((q 2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q 2) / |.q.|) - sn) / (1 + sn)))]| ) )
proof end;

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

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

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

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

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

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

theorem Th91: :: JGRAPH_4:91
for sn being Real
for K03 being Subset of () st K03 = { p where p is Point of () : ( p 2 >= sn * |.p.| & p 1 >= 0 ) } holds
K03 is closed
proof end;

theorem Th92: :: JGRAPH_4:92
for sn being Real
for K03 being Subset of () st K03 = { p where p is Point of () : ( p 2 <= sn * |.p.| & p 1 >= 0 ) } holds
K03 is closed
proof end;

theorem Th93: :: JGRAPH_4:93
for sn being Real
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st - 1 < sn & sn < 1 & f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 >= 0 & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th94: :: JGRAPH_4:94
for sn being Real
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st - 1 < sn & sn < 1 & f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 <= 0 & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th95: :: JGRAPH_4:95
for sn being Real
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st - 1 < sn & sn < 1 & f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 >= 0 & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th96: :: JGRAPH_4:96
for sn being Real
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st - 1 < sn & sn < 1 & f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( p 1 <= 0 & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th97: :: JGRAPH_4:97
for sn being Real
for p being Point of () holds |.(() . p).| = |.p.|
proof end;

theorem Th98: :: JGRAPH_4:98
for sn being Real
for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of () : ( p 1 >= 0 & p <> 0. () ) } holds
() . x in K0
proof end;

theorem Th99: :: JGRAPH_4:99
for sn being Real
for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of () : ( p 1 <= 0 & p <> 0. () ) } holds
() . x in K0
proof end;

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

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

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

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

theorem Th104: :: JGRAPH_4:104
for sn being Real
for p2 being Point of () st - 1 < sn & sn < 1 holds
ex K being non empty compact Subset of () st
( K = () .: K & ex V2 being Subset of () st
( p2 in V2 & V2 is open & V2 c= K & () . p2 in V2 ) )
proof end;

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

theorem Th106: :: JGRAPH_4:106
for sn being Real
for q being Point of () st sn < 1 & q 1 > 0 & (q 2) / |.q.| >= sn holds
for p being Point of () st p = () . q holds
( p 1 > 0 & p 2 >= 0 )
proof end;

theorem Th107: :: JGRAPH_4:107
for sn being Real
for q being Point of () st - 1 < sn & q 1 > 0 & (q 2) / |.q.| < sn holds
for p being Point of () st p = () . q holds
( p 1 > 0 & p 2 < 0 )
proof end;

theorem Th108: :: JGRAPH_4:108
for sn being Real
for q1, q2 being Point of () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 2) / |.p1.| < (p2 2) / |.p2.|
proof end;

theorem Th109: :: JGRAPH_4:109
for sn being Real
for q1, q2 being Point of () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 2) / |.p1.| < (p2 2) / |.p2.|
proof end;

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

theorem :: JGRAPH_4:111
for sn being Real
for q being Point of () st q 1 > 0 & (q 2) / |.q.| = sn holds
for p being Point of () st p = () . q holds
( p 1 > 0 & p 2 = 0 )
proof end;

theorem :: JGRAPH_4:112
for sn being Real holds 0. () = () . (0. ()) by ;

definition
let s be Real;
let q be Point of ();
func FanS (s,q) -> Point of () equals :Def8: :: 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;
correctness
coherence
( ( (q 1) / |.q.| >= s & q 2 < 0 implies |.q.| * |[((((q 1) / |.q.|) - s) / (1 - s)),(- (sqrt (1 - (((((q 1) / |.q.|) - s) / (1 - s)) ^2))))]| is Point of () ) & ( (q 1) / |.q.| < s & q 2 < 0 implies |.q.| * |[((((q 1) / |.q.|) - s) / (1 + s)),(- (sqrt (1 - (((((q 1) / |.q.|) - s) / (1 + s)) ^2))))]| is Point of () ) & ( ( not (q 1) / |.q.| >= s or not q 2 < 0 ) & ( not (q 1) / |.q.| < s or not q 2 < 0 ) implies q is Point of () ) )
;
consistency
for b1 being Point of () st (q 1) / |.q.| >= s & q 2 < 0 & (q 1) / |.q.| < s & q 2 < 0 holds
( b1 = |.q.| * |[((((q 1) / |.q.|) - s) / (1 - s)),(- (sqrt (1 - (((((q 1) / |.q.|) - s) / (1 - s)) ^2))))]| iff b1 = |.q.| * |[((((q 1) / |.q.|) - s) / (1 + s)),(- (sqrt (1 - (((((q 1) / |.q.|) - s) / (1 + s)) ^2))))]| )
;
;
end;

:: deftheorem Def8 defines FanS JGRAPH_4:def 8 :
for s being Real
for q being Point of () holds
( ( (q 1) / |.q.| >= s & q 2 < 0 implies FanS (s,q) = |.q.| * |[((((q 1) / |.q.|) - s) / (1 - s)),(- (sqrt (1 - (((((q 1) / |.q.|) - s) / (1 - s)) ^2))))]| ) & ( (q 1) / |.q.| < s & q 2 < 0 implies FanS (s,q) = |.q.| * |[((((q 1) / |.q.|) - s) / (1 + s)),(- (sqrt (1 - (((((q 1) / |.q.|) - s) / (1 + s)) ^2))))]| ) & ( ( not (q 1) / |.q.| >= s or not q 2 < 0 ) & ( not (q 1) / |.q.| < s or not q 2 < 0 ) implies FanS (s,q) = q ) );

definition
let c be Real;
func c -FanMorphS -> Function of (),() means :Def9: :: JGRAPH_4:def 9
for q being Point of () holds it . q = FanS (c,q);
existence
ex b1 being Function of (),() st
for q being Point of () holds b1 . q = FanS (c,q)
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for q being Point of () holds b1 . q = FanS (c,q) ) & ( for q being Point of () holds b2 . q = FanS (c,q) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines -FanMorphS JGRAPH_4:def 9 :
for c being Real
for b2 being Function of (),() holds
( b2 = c -FanMorphS iff for q being Point of () holds b2 . q = FanS (c,q) );

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

theorem Th114: :: JGRAPH_4:114
for q being Point of ()
for cn being Real st (q 1) / |.q.| <= cn & q 2 < 0 holds
() . q = |[(|.q.| * ((((q 1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q 1) / |.q.|) - cn) / (1 + cn)) ^2)))))]|
proof end;

theorem Th115: :: JGRAPH_4:115
for q being Point of ()
for cn being Real st - 1 < cn & cn < 1 holds
( ( (q 1) / |.q.| >= cn & q 2 <= 0 & q <> 0. () implies () . 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. () implies () . q = |[(|.q.| * ((((q 1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q 1) / |.q.|) - cn) / (1 + cn)) ^2)))))]| ) )
proof end;

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

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

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

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

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

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

theorem Th122: :: JGRAPH_4:122
for cn being Real
for K03 being Subset of () st K03 = { p where p is Point of () : ( p 1 >= cn * |.p.| & p 2 <= 0 ) } holds
K03 is closed
proof end;

theorem Th123: :: JGRAPH_4:123
for cn being Real
for K03 being Subset of () st K03 = { p where p is Point of () : ( p 1 <= cn * |.p.| & p 2 <= 0 ) } holds
K03 is closed
proof end;

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

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

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

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

theorem Th128: :: JGRAPH_4:128
for cn being Real
for p being Point of () holds |.(() . p).| = |.p.|
proof end;

theorem Th129: :: JGRAPH_4:129
for cn being Real
for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of () : ( p 2 <= 0 & p <> 0. () ) } holds
() . x in K0
proof end;

theorem Th130: :: JGRAPH_4:130
for cn being Real
for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of () : ( p 2 >= 0 & p <> 0. () ) } holds
() . x in K0
proof end;

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

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

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

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

theorem Th135: :: JGRAPH_4:135
for cn being Real
for p2 being Point of () st - 1 < cn & cn < 1 holds
ex K being non empty compact Subset of () st
( K = () .: K & ex V2 being Subset of () st
( p2 in V2 & V2 is open & V2 c= K & () . p2 in V2 ) )
proof end;

theorem :: JGRAPH_4:136
for cn being Real st - 1 < cn & cn < 1 holds
ex f being Function of (),() st
( f = cn -FanMorphS & f is being_homeomorphism )
proof end;

theorem Th137: :: JGRAPH_4:137
for cn being Real
for q being Point of () st cn < 1 & q 2 < 0 & (q 1) / |.q.| >= cn holds
for p being Point of () st p = () . q holds
( p 2 < 0 & p 1 >= 0 )
proof end;

theorem Th138: :: JGRAPH_4:138
for cn being Real
for q being Point of () st - 1 < cn & q 2 < 0 & (q 1) / |.q.| < cn holds
for p being Point of () st p = () . q holds
( p 2 < 0 & p 1 < 0 )
proof end;

theorem Th139: :: JGRAPH_4:139
for cn being Real
for q1, q2 being Point of () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 1) / |.p1.| < (p2 1) / |.p2.|
proof end;

theorem Th140: :: JGRAPH_4:140
for cn being Real
for q1, q2 being Point of () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 1) / |.p1.| < (p2 1) / |.p2.|
proof end;

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

theorem :: JGRAPH_4:142
for cn being Real
for q being Point of () st q 2 < 0 & (q 1) / |.q.| = cn holds
for p being Point of () st p = () . q holds
( p 2 < 0 & p 1 = 0 )
proof end;

theorem :: JGRAPH_4:143
for a being Real holds 0. () = () . (0. ()) by ;