:: Fan Homeomorphisms in the Plane :: by Yatsuka Nakamura :: :: Received January 8, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users begin Lm1: for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds |.p.| > 0 proofend; 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 number st g is continuous & B = { p where p is Point of X : g /. p > a } holds B is open proofend; 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 proofend; 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 proofend; 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 number 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 number st f1 . p = r1 & f2 . p = r2 holds g . p = ((r1 / r2) - a) / b ) & g is continuous ) proofend; 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 ) proofend; 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 number st f1 . p = r1 holds g . p = r1 ^2 ) & g is continuous ) proofend; 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 number st f1 . p = r1 holds g . p = abs r1 ) & g is continuous ) proofend; 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 number st f1 . p = r1 holds g . p = - r1 ) & g is continuous ) proofend; 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 number 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 number st f1 . p = r1 & f2 . p = r2 holds g . p = r2 * (- (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2))))) ) & g is continuous ) proofend; 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 number 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 number st f1 . p = r1 & f2 . p = r2 holds g . p = r2 * (sqrt (abs (1 - ((((r1 / r2) - a) / b) ^2)))) ) & g is continuous ) proofend; definition let n be Nat; deffunc H1( Point of (TOP-REAL n)) -> Element of REAL = |.$1.|; funcn 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 ex b1 being Function of (TOP-REAL n),R^1 st for q being Point of (TOP-REAL n) holds b1 . q = |.q.| proofend; uniqueness for b1, b2 being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds b1 . q = |.q.| ) & ( for q being Point of (TOP-REAL n) holds b2 . q = |.q.| ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines NormF JGRAPH_4:def_1_:_ for n being Nat for b2 being Function of (TOP-REAL n),R^1 holds ( b2 = n NormF iff for q being Point of (TOP-REAL n) holds b2 . q = |.q.| ); theorem :: JGRAPH_4:11 for n being Nat holds ( dom (n NormF) = the carrier of (TOP-REAL n) & dom (n NormF) = REAL n ) proofend; theorem Th12: :: JGRAPH_4:12 for n being Nat holds n NormF is continuous proofend; registration let n be Nat; clustern NormF -> continuous ; coherence n NormF is continuous by Th12; 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 proofend; 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 ) proofend; 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 proofend; begin definition let s be real number ; 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 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 b1 being Point of (TOP-REAL 2) st (q `2) / |.q.| >= s & q `1 < 0 & (q `2) / |.q.| < s & q `1 < 0 holds ( b1 = |.q.| * |[(- (sqrt (1 - (((((q `2) / |.q.|) - s) / (1 - s)) ^2)))),((((q `2) / |.q.|) - s) / (1 - s))]| iff b1 = |.q.| * |[(- (sqrt (1 - (((((q `2) / |.q.|) - s) / (1 + s)) ^2)))),((((q `2) / |.q.|) - s) / (1 + s))]| ); ; end; :: deftheorem Def2 defines FanW JGRAPH_4:def_2_:_ for s being real number 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 number ; funcs -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 ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st for q being Point of (TOP-REAL 2) holds b1 . q = FanW (s,q) proofend; uniqueness for b1, b2 being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of (TOP-REAL 2) holds b1 . q = FanW (s,q) ) & ( for q being Point of (TOP-REAL 2) holds b2 . q = FanW (s,q) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines -FanMorphW JGRAPH_4:def_3_:_ for s being real number for b2 being Function of (TOP-REAL 2),(TOP-REAL 2) holds ( b2 = s -FanMorphW iff for q being Point of (TOP-REAL 2) holds b2 . q = FanW (s,q) ); theorem Th16: :: JGRAPH_4:16 for q being Point of (TOP-REAL 2) for sn being real number 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 ) ) proofend; 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)))]| proofend; 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)))]| ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 ) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th33: :: JGRAPH_4:33 for sn being Real for p being Point of (TOP-REAL 2) holds |.((sn -FanMorphW) . p).| = |.p.| proofend; 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 proofend; 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 proofend; scheme :: JGRAPH_4:sch 1 InclSub{ F1() -> non empty Subset of (TOP-REAL 2), P1[ set ] } : { p where p is Point of (TOP-REAL 2) : ( P1[p] & p <> 0. (TOP-REAL 2) ) } c= the carrier of ((TOP-REAL 2) | F1()) provided A1: F1() = NonZero (TOP-REAL 2) proofend; 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 ) proofend; 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 ) proofend; theorem Th38: :: JGRAPH_4:38 for sn being Real st - 1 < sn & sn < 1 holds sn -FanMorphW is one-to-one proofend; 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) ) proofend; 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)) proofend; 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 ) ) proofend; 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 ) proofend; 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 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; 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 ) proofend; 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 ) proofend; 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.| proofend; 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.| proofend; 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.| proofend; 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 ) proofend; theorem :: JGRAPH_4:48 for sn being real number holds 0. (TOP-REAL 2) = (sn -FanMorphW) . (0. (TOP-REAL 2)) by Th16, JGRAPH_2:3; begin definition let s be real number ; 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 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 b1 being Point of (TOP-REAL 2) st (q `1) / |.q.| >= s & q `2 > 0 & (q `1) / |.q.| < s & q `2 > 0 holds ( b1 = |.q.| * |[((((q `1) / |.q.|) - s) / (1 - s)),(sqrt (1 - (((((q `1) / |.q.|) - s) / (1 - s)) ^2)))]| iff b1 = |.q.| * |[((((q `1) / |.q.|) - s) / (1 + s)),(sqrt (1 - (((((q `1) / |.q.|) - s) / (1 + s)) ^2)))]| ); ; end; :: deftheorem Def4 defines FanN JGRAPH_4:def_4_:_ for s being real number 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 number ; funcc -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 ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st for q being Point of (TOP-REAL 2) holds b1 . q = FanN (c,q) proofend; uniqueness for b1, b2 being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of (TOP-REAL 2) holds b1 . q = FanN (c,q) ) & ( for q being Point of (TOP-REAL 2) holds b2 . q = FanN (c,q) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines -FanMorphN JGRAPH_4:def_5_:_ for c being real number for b2 being Function of (TOP-REAL 2),(TOP-REAL 2) holds ( b2 = c -FanMorphN iff for q being Point of (TOP-REAL 2) holds b2 . q = FanN (c,q) ); theorem Th49: :: JGRAPH_4:49 for q being Point of (TOP-REAL 2) for cn being real number 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 ) ) proofend; 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))))]| proofend; 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))))]| ) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th66: :: JGRAPH_4:66 for cn being Real for p being Point of (TOP-REAL 2) holds |.((cn -FanMorphN) . p).| = |.p.| proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; theorem Th71: :: JGRAPH_4:71 for cn being Real st - 1 < cn & cn < 1 holds cn -FanMorphN is one-to-one proofend; 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) ) proofend; 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 ) ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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.| proofend; 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.| proofend; 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.| proofend; 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 ) proofend; theorem :: JGRAPH_4:81 for cn being real number holds 0. (TOP-REAL 2) = (cn -FanMorphN) . (0. (TOP-REAL 2)) by Th49, JGRAPH_2:3; begin definition let s be real number ; 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 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 b1 being Point of (TOP-REAL 2) st (q `2) / |.q.| >= s & q `1 > 0 & (q `2) / |.q.| < s & q `1 > 0 holds ( b1 = |.q.| * |[(sqrt (1 - (((((q `2) / |.q.|) - s) / (1 - s)) ^2))),((((q `2) / |.q.|) - s) / (1 - s))]| iff b1 = |.q.| * |[(sqrt (1 - (((((q `2) / |.q.|) - s) / (1 + s)) ^2))),((((q `2) / |.q.|) - s) / (1 + s))]| ); ; end; :: deftheorem Def6 defines FanE JGRAPH_4:def_6_:_ for s being real number 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 number ; funcs -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 ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st for q being Point of (TOP-REAL 2) holds b1 . q = FanE (s,q) proofend; uniqueness for b1, b2 being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of (TOP-REAL 2) holds b1 . q = FanE (s,q) ) & ( for q being Point of (TOP-REAL 2) holds b2 . q = FanE (s,q) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines -FanMorphE JGRAPH_4:def_7_:_ for s being real number for b2 being Function of (TOP-REAL 2),(TOP-REAL 2) holds ( b2 = s -FanMorphE iff for q being Point of (TOP-REAL 2) holds b2 . q = FanE (s,q) ); theorem Th82: :: JGRAPH_4:82 for q being Point of (TOP-REAL 2) for sn being real number 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 ) ) proofend; 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)))]| proofend; 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)))]| ) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th97: :: JGRAPH_4:97 for sn being Real for p being Point of (TOP-REAL 2) holds |.((sn -FanMorphE) . p).| = |.p.| proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; theorem Th102: :: JGRAPH_4:102 for sn being Real st - 1 < sn & sn < 1 holds sn -FanMorphE is one-to-one proofend; 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) ) proofend; 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 ) ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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.| proofend; 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.| proofend; 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.| proofend; 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 ) proofend; theorem :: JGRAPH_4:112 for sn being real number holds 0. (TOP-REAL 2) = (sn -FanMorphE) . (0. (TOP-REAL 2)) by Th82, JGRAPH_2:3; begin definition let s be real number ; 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 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 b1 being Point of (TOP-REAL 2) st (q `1) / |.q.| >= s & q `2 < 0 & (q `1) / |.q.| < s & q `2 < 0 holds ( b1 = |.q.| * |[((((q `1) / |.q.|) - s) / (1 - s)),(- (sqrt (1 - (((((q `1) / |.q.|) - s) / (1 - s)) ^2))))]| iff b1 = |.q.| * |[((((q `1) / |.q.|) - s) / (1 + s)),(- (sqrt (1 - (((((q `1) / |.q.|) - s) / (1 + s)) ^2))))]| ); ; end; :: deftheorem Def8 defines FanS JGRAPH_4:def_8_:_ for s being real number 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 number ; funcc -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 ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st for q being Point of (TOP-REAL 2) holds b1 . q = FanS (c,q) proofend; uniqueness for b1, b2 being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for q being Point of (TOP-REAL 2) holds b1 . q = FanS (c,q) ) & ( for q being Point of (TOP-REAL 2) holds b2 . q = FanS (c,q) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines -FanMorphS JGRAPH_4:def_9_:_ for c being real number for b2 being Function of (TOP-REAL 2),(TOP-REAL 2) holds ( b2 = c -FanMorphS iff for q being Point of (TOP-REAL 2) holds b2 . q = FanS (c,q) ); theorem Th113: :: JGRAPH_4:113 for q being Point of (TOP-REAL 2) for cn being real number 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 ) ) proofend; 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)))))]| proofend; 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)))))]| ) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem Th128: :: JGRAPH_4:128 for cn being Real for p being Point of (TOP-REAL 2) holds |.((cn -FanMorphS) . p).| = |.p.| proofend; 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 proofend; 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 proofend; 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 ) proofend; theorem Th132: :: JGRAPH_4:132 for cn being Real st - 1 < cn & cn < 1 holds cn -FanMorphS is continuous proofend; theorem Th133: :: JGRAPH_4:133 for cn being Real st - 1 < cn & cn < 1 holds cn -FanMorphS is one-to-one proofend; 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) ) proofend; 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 ) ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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.| proofend; 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.| proofend; 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.| proofend; 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 ) proofend; theorem :: JGRAPH_4:143 for a being real number holds 0. (TOP-REAL 2) = (a -FanMorphS) . (0. (TOP-REAL 2)) by Th113, JGRAPH_2:3;