:: by Yatsuka Nakamura

::

:: Received January 8, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

Lm1: for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) 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

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

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 (TOP-REAL 2),(TOP-REAL 2) st f is continuous & f is 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

( 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

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 H_{1}( Point of (TOP-REAL n)) -> object = |.$1.|;

ex b_{1} being Function of (TOP-REAL n),R^1 st

for q being Point of (TOP-REAL n) holds b_{1} . q = |.q.|

for b_{1}, b_{2} being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds b_{1} . q = |.q.| ) & ( for q being Point of (TOP-REAL n) holds b_{2} . q = |.q.| ) holds

b_{1} = b_{2}

end;
deffunc H

func n NormF -> Function of (TOP-REAL n),R^1 means :Def1: :: JGRAPH_4:def 1

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

existence for q being Point of (TOP-REAL n) holds it . q = |.q.|;

ex b

for q being Point of (TOP-REAL n) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines NormF JGRAPH_4:def 1 :

for n being Nat

for b_{2} being Function of (TOP-REAL n),R^1 holds

( b_{2} = n NormF iff for q being Point of (TOP-REAL n) holds b_{2} . q = |.q.| );

for n being Nat

for b

( b

registration
end;

theorem Th13: :: JGRAPH_4:13

for n being Element of NAT

for K0 being Subset of (TOP-REAL n)

for 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

for K0 being Subset of (TOP-REAL n)

for 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

proof end;

theorem Th14: :: JGRAPH_4:14

for n being Element of NAT

for p being Point of (Euclid n)

for r being Real

for B being Subset of (TOP-REAL n) st B = cl_Ball (p,r) holds

( B is bounded & B is closed )

for p being Point of (Euclid n)

for r being Real

for B being Subset of (TOP-REAL n) 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 (Euclid 2)

for r being Real

for B being Subset of (TOP-REAL 2) st B = cl_Ball (p,r) holds

B is compact

for r being Real

for B being Subset of (TOP-REAL 2) st B = cl_Ball (p,r) holds

B is compact

proof end;

definition

let s be Real;

let q be Point of (TOP-REAL 2);

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 (TOP-REAL 2) ) & ( (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 (TOP-REAL 2) ) & ( ( 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 (TOP-REAL 2) ) );

consistency

for b_{1} being Point of (TOP-REAL 2) st (q `2) / |.q.| >= s & q `1 < 0 & (q `2) / |.q.| < s & q `1 < 0 holds

( b_{1} = |.q.| * |[(- (sqrt (1 - (((((q `2) / |.q.|) - s) / (1 - s)) ^2)))),((((q `2) / |.q.|) - s) / (1 - s))]| iff b_{1} = |.q.| * |[(- (sqrt (1 - (((((q `2) / |.q.|) - s) / (1 + s)) ^2)))),((((q `2) / |.q.|) - s) / (1 + s))]| );

;

end;
let q be Point of (TOP-REAL 2);

func FanW (s,q) -> Point of (TOP-REAL 2) 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 |.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;

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 (TOP-REAL 2) ) & ( (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 (TOP-REAL 2) ) & ( ( 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 (TOP-REAL 2) ) );

consistency

for b

( b

;

:: deftheorem Def2 defines FanW JGRAPH_4:def 2 :

for s being Real

for q being Point of (TOP-REAL 2) 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 ) );

for s being Real

for q being Point of (TOP-REAL 2) 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;

ex b_{1} being Function of (TOP-REAL 2),(TOP-REAL 2) st

for q being Point of (TOP-REAL 2) holds b_{1} . q = FanW (s,q)

for b_{1}, b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of (TOP-REAL 2) holds b_{1} . q = FanW (s,q) ) & ( for q being Point of (TOP-REAL 2) holds b_{2} . q = FanW (s,q) ) holds

b_{1} = b_{2}

end;
func s -FanMorphW -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def3: :: JGRAPH_4:def 3

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

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

ex b

for q being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines -FanMorphW JGRAPH_4:def 3 :

for s being Real

for b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) holds

( b_{2} = s -FanMorphW iff for q being Point of (TOP-REAL 2) holds b_{2} . q = FanW (s,q) );

for s being Real

for b

( b

theorem Th16: :: JGRAPH_4:16

for q being Point of (TOP-REAL 2)

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

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

proof end;

theorem Th17: :: JGRAPH_4:17

for q being Point of (TOP-REAL 2)

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

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

proof end;

theorem Th18: :: JGRAPH_4:18

for q being Point of (TOP-REAL 2)

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

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

proof end;

Lm2: for K being non empty Subset of (TOP-REAL 2) holds

( proj1 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds (proj1 | K) . q = proj1 . q ) )

proof end;

Lm3: for K being non empty Subset of (TOP-REAL 2) holds

( proj2 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds (proj2 | K) . q = proj2 . q ) )

proof end;

Lm4: dom (2 NormF) = the carrier of (TOP-REAL 2)

by FUNCT_2:def 1;

Lm5: for K being non empty Subset of (TOP-REAL 2) holds

( (2 NormF) | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds ((2 NormF) | K) . q = (2 NormF) . q ) )

proof end;

Lm6: for K1 being non empty Subset of (TOP-REAL 2)

for g1 being Function of ((TOP-REAL 2) | K1),R^1 st g1 = (2 NormF) | K1 & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q <> 0. (TOP-REAL 2) ) holds

for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0

proof end;

theorem Th19: :: JGRAPH_4:19

for sn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th20: :: JGRAPH_4:20

for sn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th21: :: JGRAPH_4:21

for sn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th22: :: JGRAPH_4:22

for sn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th23: :: JGRAPH_4:23

for sn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| >= sn & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| >= sn & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th24: :: JGRAPH_4:24

for sn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

Lm7: for sn being Real

for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 >= sn * |.p7.| } holds

K1 is closed

proof end;

Lm8: for sn being Real

for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 >= sn * |.p7.| } holds

K1 is closed

proof end;

theorem Th25: :: JGRAPH_4:25

for sn being Real

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= sn * |.p.| & p `1 <= 0 ) } holds

K03 is closed

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= sn * |.p.| & p `1 <= 0 ) } holds

K03 is closed

proof end;

Lm9: for sn being Real

for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= sn * |.p7.| } holds

K1 is closed

proof end;

Lm10: for sn being Real

for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= sn * |.p7.| } holds

K1 is closed

proof end;

theorem Th26: :: JGRAPH_4:26

for sn being Real

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `2 <= sn * |.p.| & p `1 <= 0 ) } holds

K03 is closed

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th28: :: JGRAPH_4:28

for sn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th29: :: JGRAPH_4:29

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

K0 is closed

for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

K0 is closed

proof end;

theorem Th30: :: JGRAPH_4:30

for sn being Real

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th31: :: JGRAPH_4:31

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

K0 is closed

for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

K0 is closed

proof end;

theorem Th32: :: JGRAPH_4:32

for sn being Real

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

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 (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

(sn -FanMorphW) . x in K0

for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

(sn -FanMorphW) . 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 (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

(sn -FanMorphW) . x in K0

for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

(sn -FanMorphW) . x in K0

proof end;

theorem Th36: :: JGRAPH_4:36

for sn being Real

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

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

proof end;

Lm11: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)

by EUCLID:def 8;

theorem Th37: :: 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 )

ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st

( h = sn -FanMorphW & h is continuous )

proof end;

theorem Th39: :: 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) )

( sn -FanMorphW is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (sn -FanMorphW) = the carrier of (TOP-REAL 2) )

proof end;

Lm12: for q4, q, p2 being Point of (TOP-REAL 2)

for O, u, uq being Point of (Euclid 2) st u in cl_Ball (O,(|.p2.| + 1)) & q = uq & q4 = u & O = 0. (TOP-REAL 2) & |.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 (TOP-REAL 2) st - 1 < sn & sn < 1 holds

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

for p2 being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 holds

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

proof end;

theorem :: JGRAPH_4:41

for sn being Real st - 1 < sn & sn < 1 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st

( f = sn -FanMorphW & f is being_homeomorphism )

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st

( f = sn -FanMorphW & f is being_homeomorphism )

proof end;

Lm13: now :: thesis: for q being Point of (TOP-REAL 2)

for sn, t being Real st ((- ((t / |.q.|) - sn)) / (1 - sn)) ^2 < 1 ^2 holds

- (sqrt (1 - ((((t / |.q.|) - sn) / (1 - sn)) ^2))) < - 0

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 (TOP-REAL 2); :: 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;
- (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

theorem Th42: :: JGRAPH_4:42

for sn being Real

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

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

proof end;

theorem Th43: :: JGRAPH_4:43

for sn being Real

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

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

proof end;

theorem Th44: :: JGRAPH_4:44

for sn being Real

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

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

proof end;

theorem Th45: :: JGRAPH_4:45

for sn being Real

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

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

proof end;

theorem :: JGRAPH_4:46

for sn being Real

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

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

proof end;

theorem :: JGRAPH_4:47

for sn being Real

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

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

proof end;

theorem :: JGRAPH_4:48

definition

let s be Real;

let q be Point of (TOP-REAL 2);

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 (TOP-REAL 2) ) & ( (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 (TOP-REAL 2) ) & ( ( 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 (TOP-REAL 2) ) );

consistency

for b_{1} being Point of (TOP-REAL 2) st (q `1) / |.q.| >= s & q `2 > 0 & (q `1) / |.q.| < s & q `2 > 0 holds

( b_{1} = |.q.| * |[((((q `1) / |.q.|) - s) / (1 - s)),(sqrt (1 - (((((q `1) / |.q.|) - s) / (1 - s)) ^2)))]| iff b_{1} = |.q.| * |[((((q `1) / |.q.|) - s) / (1 + s)),(sqrt (1 - (((((q `1) / |.q.|) - s) / (1 + s)) ^2)))]| );

;

end;
let q be Point of (TOP-REAL 2);

func FanN (s,q) -> Point of (TOP-REAL 2) 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 |.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;

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 (TOP-REAL 2) ) & ( (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 (TOP-REAL 2) ) & ( ( 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 (TOP-REAL 2) ) );

consistency

for b

( b

;

:: deftheorem Def4 defines FanN JGRAPH_4:def 4 :

for s being Real

for q being Point of (TOP-REAL 2) 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 ) );

for s being Real

for q being Point of (TOP-REAL 2) 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;

ex b_{1} being Function of (TOP-REAL 2),(TOP-REAL 2) st

for q being Point of (TOP-REAL 2) holds b_{1} . q = FanN (c,q)

for b_{1}, b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of (TOP-REAL 2) holds b_{1} . q = FanN (c,q) ) & ( for q being Point of (TOP-REAL 2) holds b_{2} . q = FanN (c,q) ) holds

b_{1} = b_{2}

end;
func c -FanMorphN -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def5: :: JGRAPH_4:def 5

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

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

ex b

for q being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines -FanMorphN JGRAPH_4:def 5 :

for c being Real

for b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) holds

( b_{2} = c -FanMorphN iff for q being Point of (TOP-REAL 2) holds b_{2} . q = FanN (c,q) );

for c being Real

for b

( b

theorem Th49: :: JGRAPH_4:49

for q being Point of (TOP-REAL 2)

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

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

proof end;

theorem Th50: :: JGRAPH_4:50

for q being Point of (TOP-REAL 2)

for cn being Real st (q `1) / |.q.| <= cn & q `2 > 0 holds

(cn -FanMorphN) . q = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2))))]|

for cn being Real st (q `1) / |.q.| <= cn & q `2 > 0 holds

(cn -FanMorphN) . 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 (TOP-REAL 2)

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

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

proof end;

theorem Th52: :: JGRAPH_4:52

for cn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th53: :: JGRAPH_4:53

for cn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th54: :: JGRAPH_4:54

for cn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th55: :: JGRAPH_4:55

for cn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th56: :: JGRAPH_4:56

for cn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th57: :: JGRAPH_4:57

for cn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th58: :: JGRAPH_4:58

for cn being Real

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= cn * |.p.| & p `2 >= 0 ) } holds

K03 is closed

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= cn * |.p.| & p `2 >= 0 ) } holds

K03 is closed

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th61: :: JGRAPH_4:61

for cn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th62: :: JGRAPH_4:62

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

K0 is closed

for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

K0 is closed

proof end;

theorem Th63: :: JGRAPH_4:63

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

K0 is closed

for K0 being Subset of ((TOP-REAL 2) | B0) st B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

K0 is closed

proof end;

theorem Th64: :: JGRAPH_4:64

for cn being Real

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th65: :: JGRAPH_4:65

for cn being Real

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

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 (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

(cn -FanMorphN) . x in K0

for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

(cn -FanMorphN) . 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 (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

(cn -FanMorphN) . x in K0

for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

(cn -FanMorphN) . x in K0

proof end;

theorem Th69: :: JGRAPH_4:69

for cn being Real

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

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

proof end;

theorem Th70: :: 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 )

ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st

( h = cn -FanMorphN & h is continuous )

proof end;

theorem Th72: :: 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) )

( cn -FanMorphN is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (cn -FanMorphN) = the carrier of (TOP-REAL 2) )

proof end;

theorem Th73: :: JGRAPH_4:73

for cn being Real

for p2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 holds

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

for p2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 holds

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

proof end;

theorem :: JGRAPH_4:74

for cn being Real st - 1 < cn & cn < 1 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st

( f = cn -FanMorphN & f is being_homeomorphism )

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st

( f = cn -FanMorphN & f is being_homeomorphism )

proof end;

theorem Th75: :: JGRAPH_4:75

for cn being Real

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

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

proof end;

theorem Th76: :: JGRAPH_4:76

for cn being Real

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

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

proof end;

theorem Th77: :: JGRAPH_4:77

for cn being Real

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

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

proof end;

theorem Th78: :: JGRAPH_4:78

for cn being Real

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

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

proof end;

theorem :: JGRAPH_4:79

for cn being Real

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

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

proof end;

theorem :: JGRAPH_4:80

for cn being Real

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

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

proof end;

theorem :: JGRAPH_4:81

definition

let s be Real;

let q be Point of (TOP-REAL 2);

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 (TOP-REAL 2) ) & ( (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 (TOP-REAL 2) ) & ( ( 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 (TOP-REAL 2) ) );

consistency

for b_{1} being Point of (TOP-REAL 2) st (q `2) / |.q.| >= s & q `1 > 0 & (q `2) / |.q.| < s & q `1 > 0 holds

( b_{1} = |.q.| * |[(sqrt (1 - (((((q `2) / |.q.|) - s) / (1 - s)) ^2))),((((q `2) / |.q.|) - s) / (1 - s))]| iff b_{1} = |.q.| * |[(sqrt (1 - (((((q `2) / |.q.|) - s) / (1 + s)) ^2))),((((q `2) / |.q.|) - s) / (1 + s))]| );

;

end;
let q be Point of (TOP-REAL 2);

func FanE (s,q) -> Point of (TOP-REAL 2) 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 |.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;

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 (TOP-REAL 2) ) & ( (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 (TOP-REAL 2) ) & ( ( 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 (TOP-REAL 2) ) );

consistency

for b

( b

;

:: deftheorem Def6 defines FanE JGRAPH_4:def 6 :

for s being Real

for q being Point of (TOP-REAL 2) 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 ) );

for s being Real

for q being Point of (TOP-REAL 2) 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;

ex b_{1} being Function of (TOP-REAL 2),(TOP-REAL 2) st

for q being Point of (TOP-REAL 2) holds b_{1} . q = FanE (s,q)

for b_{1}, b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of (TOP-REAL 2) holds b_{1} . q = FanE (s,q) ) & ( for q being Point of (TOP-REAL 2) holds b_{2} . q = FanE (s,q) ) holds

b_{1} = b_{2}

end;
func s -FanMorphE -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def7: :: JGRAPH_4:def 7

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

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

ex b

for q being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines -FanMorphE JGRAPH_4:def 7 :

for s being Real

for b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) holds

( b_{2} = s -FanMorphE iff for q being Point of (TOP-REAL 2) holds b_{2} . q = FanE (s,q) );

for s being Real

for b

( b

theorem Th82: :: JGRAPH_4:82

for q being Point of (TOP-REAL 2)

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

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

proof end;

theorem Th83: :: JGRAPH_4:83

for q being Point of (TOP-REAL 2)

for sn being Real st (q `2) / |.q.| <= sn & q `1 > 0 holds

(sn -FanMorphE) . q = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 + sn)))]|

for sn being Real st (q `2) / |.q.| <= sn & q `1 > 0 holds

(sn -FanMorphE) . 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 (TOP-REAL 2)

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

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

proof end;

theorem Th85: :: JGRAPH_4:85

for sn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th86: :: JGRAPH_4:86

for sn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th87: :: JGRAPH_4:87

for sn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th88: :: JGRAPH_4:88

for sn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th89: :: JGRAPH_4:89

for sn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| >= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| >= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th90: :: JGRAPH_4:90

for sn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `2) / |.p.| <= sn & p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th91: :: JGRAPH_4:91

for sn being Real

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= sn * |.p.| & p `1 >= 0 ) } holds

K03 is closed

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `2 <= sn * |.p.| & p `1 >= 0 ) } holds

K03 is closed

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th94: :: JGRAPH_4:94

for sn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th95: :: JGRAPH_4:95

for sn being Real

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th96: :: JGRAPH_4:96

for sn being Real

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

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 (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

(sn -FanMorphE) . x in K0

for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

(sn -FanMorphE) . 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 (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

(sn -FanMorphE) . x in K0

for x, K0 being set st - 1 < sn & sn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

(sn -FanMorphE) . x in K0

proof end;

theorem Th100: :: JGRAPH_4:100

for sn being Real

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

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

proof end;

theorem Th101: :: 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 )

ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st

( h = sn -FanMorphE & h is continuous )

proof end;

theorem Th103: :: 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) )

( sn -FanMorphE is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (sn -FanMorphE) = the carrier of (TOP-REAL 2) )

proof end;

theorem Th104: :: JGRAPH_4:104

for sn being Real

for p2 being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 holds

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

for p2 being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 holds

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

proof end;

theorem :: JGRAPH_4:105

for sn being Real st - 1 < sn & sn < 1 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st

( f = sn -FanMorphE & f is being_homeomorphism )

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st

( f = sn -FanMorphE & f is being_homeomorphism )

proof end;

theorem Th106: :: JGRAPH_4:106

for sn being Real

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

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

proof end;

theorem Th107: :: JGRAPH_4:107

for sn being Real

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

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

proof end;

theorem Th108: :: JGRAPH_4:108

for sn being Real

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

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

proof end;

theorem Th109: :: JGRAPH_4:109

for sn being Real

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

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

proof end;

theorem :: JGRAPH_4:110

for sn being Real

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

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

proof end;

theorem :: JGRAPH_4:111

for sn being Real

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

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

proof end;

theorem :: JGRAPH_4:112

definition

let s be Real;

let q be Point of (TOP-REAL 2);

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 (TOP-REAL 2) ) & ( (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 (TOP-REAL 2) ) & ( ( 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 (TOP-REAL 2) ) );

consistency

for b_{1} being Point of (TOP-REAL 2) st (q `1) / |.q.| >= s & q `2 < 0 & (q `1) / |.q.| < s & q `2 < 0 holds

( b_{1} = |.q.| * |[((((q `1) / |.q.|) - s) / (1 - s)),(- (sqrt (1 - (((((q `1) / |.q.|) - s) / (1 - s)) ^2))))]| iff b_{1} = |.q.| * |[((((q `1) / |.q.|) - s) / (1 + s)),(- (sqrt (1 - (((((q `1) / |.q.|) - s) / (1 + s)) ^2))))]| );

;

end;
let q be Point of (TOP-REAL 2);

func FanS (s,q) -> Point of (TOP-REAL 2) 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 |.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;

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 (TOP-REAL 2) ) & ( (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 (TOP-REAL 2) ) & ( ( 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 (TOP-REAL 2) ) );

consistency

for b

( b

;

:: deftheorem Def8 defines FanS JGRAPH_4:def 8 :

for s being Real

for q being Point of (TOP-REAL 2) 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 ) );

for s being Real

for q being Point of (TOP-REAL 2) 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;

ex b_{1} being Function of (TOP-REAL 2),(TOP-REAL 2) st

for q being Point of (TOP-REAL 2) holds b_{1} . q = FanS (c,q)

for b_{1}, b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of (TOP-REAL 2) holds b_{1} . q = FanS (c,q) ) & ( for q being Point of (TOP-REAL 2) holds b_{2} . q = FanS (c,q) ) holds

b_{1} = b_{2}

end;
func c -FanMorphS -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def9: :: JGRAPH_4:def 9

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

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

ex b

for q being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines -FanMorphS JGRAPH_4:def 9 :

for c being Real

for b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) holds

( b_{2} = c -FanMorphS iff for q being Point of (TOP-REAL 2) holds b_{2} . q = FanS (c,q) );

for c being Real

for b

( b

theorem Th113: :: JGRAPH_4:113

for q being Point of (TOP-REAL 2)

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

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

proof end;

theorem Th114: :: JGRAPH_4:114

for q being Point of (TOP-REAL 2)

for cn being Real st (q `1) / |.q.| <= cn & q `2 < 0 holds

(cn -FanMorphS) . q = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]|

for cn being Real st (q `1) / |.q.| <= cn & q `2 < 0 holds

(cn -FanMorphS) . 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 (TOP-REAL 2)

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

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

proof end;

theorem Th116: :: JGRAPH_4:116

for cn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th117: :: JGRAPH_4:117

for cn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th118: :: JGRAPH_4:118

for cn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th119: :: JGRAPH_4:119

for cn being Real

for K1 being non empty Subset of (TOP-REAL 2)

for 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

for K1 being non empty Subset of (TOP-REAL 2)

for 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

proof end;

theorem Th120: :: JGRAPH_4:120

for cn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| >= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th121: :: JGRAPH_4:121

for cn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( (p `1) / |.p.| <= cn & p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th122: :: JGRAPH_4:122

for cn being Real

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= cn * |.p.| & p `2 <= 0 ) } holds

K03 is closed

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= cn * |.p.| & p `2 <= 0 ) } holds

K03 is closed

for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th125: :: JGRAPH_4:125

for cn being Real

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for K0, B0 being Subset of (TOP-REAL 2)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th126: :: JGRAPH_4:126

for cn being Real

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th127: :: JGRAPH_4:127

for cn being Real

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for 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 where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

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 (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

(cn -FanMorphS) . x in K0

for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 <= 0 & p <> 0. (TOP-REAL 2) ) } holds

(cn -FanMorphS) . 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 (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

(cn -FanMorphS) . x in K0

for x, K0 being set st - 1 < cn & cn < 1 & x in K0 & K0 = { p where p is Point of (TOP-REAL 2) : ( p `2 >= 0 & p <> 0. (TOP-REAL 2) ) } holds

(cn -FanMorphS) . x in K0

proof end;

theorem Th131: :: JGRAPH_4:131

for cn being Real

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

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

proof end;

theorem Th134: :: 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) )

( cn -FanMorphS is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (cn -FanMorphS) = the carrier of (TOP-REAL 2) )

proof end;

theorem Th135: :: JGRAPH_4:135

for cn being Real

for p2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 holds

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

for p2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 holds

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

proof end;

theorem :: JGRAPH_4:136

for cn being Real st - 1 < cn & cn < 1 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st

( f = cn -FanMorphS & f is being_homeomorphism )

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st

( f = cn -FanMorphS & f is being_homeomorphism )

proof end;

theorem Th137: :: JGRAPH_4:137

for cn being Real

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

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

proof end;

theorem Th138: :: JGRAPH_4:138

for cn being Real

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

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

proof end;

theorem Th139: :: JGRAPH_4:139

for cn being Real

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

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

proof end;

theorem Th140: :: JGRAPH_4:140

for cn being Real

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

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

proof end;

theorem :: JGRAPH_4:141

for cn being Real

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

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

proof end;

theorem :: JGRAPH_4:142

for cn being Real

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

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

proof end;

theorem :: JGRAPH_4:143