:: JGRAPH_4 semantic presentation

Lemma1: for b₁ being Point of (TOP-REAL 2) st b₁ <> 0.REAL 2 holds
|.b₁.| > 0

proof end;

Lemma2: for b₁, b₂ being real number st b₁ >= 0 & (b₂ - b₁) * (b₂ + b₁) < 0 holds
( - b₁ < b₂ & b₂ < b₁ )
by XREAL_1:96;

theorem Th1: :: JGRAPH_4:1

canceled;

theorem Th2: :: JGRAPH_4:2

canceled;

theorem Th3: :: JGRAPH_4:3

for b₁ being real number st - 1 < b₁ & b₁ < 1 holds
( 1 + b₁ > 0 & 1 - b₁ > 0 ) by XREAL_1:150, XREAL_1:151;

theorem Th4: :: JGRAPH_4:4

for b₁ being real number st b₁ ^2 <= 1 holds
( - 1 <= b₁ & b₁ <= 1 )

proof end;

theorem Th5: :: JGRAPH_4:5

for b₁ being real number st b₁ ^2 < 1 holds
( - 1 < b₁ & b₁ < 1 )

proof end;

theorem Th6: :: JGRAPH_4:6

for b₁ being non empty TopStruct
for b₂ being Function of b₁,R^1
for b₃ being Subset of b₁
for b₄ being real number st b₂ is continuous & b₃ = { b₅ where B is Point of b₁ : pi b₂,b₅ > b₄ } holds
b₃ is open

proof end;

theorem Th7: :: JGRAPH_4:7

for b₁ being non empty TopStruct
for b₂ being Function of b₁,R^1
for b₃ being Subset of b₁
for b₄ being Real st b₂ is continuous & b₃ = { b₅ where B is Point of b₁ : pi b₂,b₅ < b₄ } holds
b₃ is open

proof end;

theorem Th8: :: JGRAPH_4:8

for b₁ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₁ is continuous & b₁ is one-to-one & rng b₁ = [#] (TOP-REAL 2) & ( for b₂ being Point of (TOP-REAL 2) ex b₃ being non empty compact Subset of (TOP-REAL 2) st
( b₃ = b₁ .: b₃ & ex b₄ being Subset of (TOP-REAL 2) st
( b₂ in b₄ & b₄ is open & b₄ c= b₃ & b₁ . b₂ in b₄ ) ) ) holds
b₁ is_homeomorphism

proof end;

theorem Th9: :: JGRAPH_4:9

for b₁ being non empty TopSpace
for b₂, b₃ being Function of b₁,R^1
for b₄, b₅ being real number st b₂ is continuous & b₃ is continuous & b₅ <> 0 & ( for b₆ being Point of b₁ holds b₃ . b₆ <> 0 ) holds
ex b₆ being Function of b₁,R^1 st
( ( for b₇ being Point of b₁
for b₈, b₉ being real number st b₂ . b₇ = b₈ & b₃ . b₇ = b₉ holds
b₆ . b₇ = ((b₈ / b₉) - b₄) / b₅ ) & b₆ is continuous )

proof end;

theorem Th10: :: JGRAPH_4:10

for b₁ being non empty TopSpace
for b₂, b₃ being Function of b₁,R^1
for b₄, b₅ being Real st b₂ is continuous & b₃ is continuous & b₅ <> 0 & ( for b₆ being Point of b₁ holds b₃ . b₆ <> 0 ) holds
ex b₆ being Function of b₁,R^1 st
( ( for b₇ being Point of b₁
for b₈, b₉ being Real st b₂ . b₇ = b₈ & b₃ . b₇ = b₉ holds
b₆ . b₇ = b₉ * (((b₈ / b₉) - b₄) / b₅) ) & b₆ is continuous )

proof end;

theorem Th11: :: JGRAPH_4:11

for b₁ being non empty TopSpace
for b₂ being Function of b₁,R^1 st b₂ is continuous holds
ex b₃ being Function of b₁,R^1 st
( ( for b₄ being Point of b₁
for b₅ being real number st b₂ . b₄ = b₅ holds
b₃ . b₄ = b₅ ^2 ) & b₃ is continuous )

proof end;

theorem Th12: :: JGRAPH_4:12

proof end;

theorem Th13: :: JGRAPH_4:13

proof end;

theorem Th14: :: JGRAPH_4:14

for b₁ being non empty TopSpace
for b₂, b₃ being Function of b₁,R^1
for b₄, b₅ being real number st b₂ is continuous & b₃ is continuous & b₅ <> 0 & ( for b₆ being Point of b₁ holds b₃ . b₆ <> 0 ) holds
ex b₆ being Function of b₁,R^1 st
( ( for b₇ being Point of b₁
for b₈, b₉ being real number st b₂ . b₇ = b₈ & b₃ . b₇ = b₉ holds
b₆ . b₇ = b₉ * (- (sqrt (abs (1 - ((((b₈ / b₉) - b₄) / b₅) ^2 ))))) ) & b₆ is continuous )

proof end;

theorem Th15: :: JGRAPH_4:15

for b₁ being non empty TopSpace
for b₂, b₃ being Function of b₁,R^1
for b₄, b₅ being real number st b₂ is continuous & b₃ is continuous & b₅ <> 0 & ( for b₆ being Point of b₁ holds b₃ . b₆ <> 0 ) holds
ex b₆ being Function of b₁,R^1 st
( ( for b₇ being Point of b₁
for b₈, b₉ being real number st b₂ . b₇ = b₈ & b₃ . b₇ = b₉ holds
b₆ . b₇ = b₉ * (sqrt (abs (1 - ((((b₈ / b₉) - b₄) / b₅) ^2 )))) ) & b₆ is continuous )

proof end;

definition

let c₁ be Nat;
func c₁ NormF -> Function of (TOP-REAL a₁),R^1 means :Def1: :: JGRAPH_4:def 1
for b₁ being Point of (TOP-REAL a₁) holds a₂ . b₁ = |.b₁.|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines NormF JGRAPH_4:def 1 :

theorem Th16: :: JGRAPH_4:16

for b₁ being Nat holds
( dom (b₁ NormF ) = the carrier of (TOP-REAL b₁) & dom (b₁ NormF ) = REAL b₁ )

proof end;

theorem Th17: :: JGRAPH_4:17

canceled;

theorem Th18: :: JGRAPH_4:18

canceled;

theorem Th19: :: JGRAPH_4:19

for b₁ being Nat
for b₂ being Function of (TOP-REAL b₁),R^1 st b₂ = b₁ NormF holds
b₂ is continuous

proof end;

theorem Th20: :: JGRAPH_4:20

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being Function of ((TOP-REAL b₁) | b₂),R^1 st ( for b₄ being Point of ((TOP-REAL b₁) | b₂) holds b₃ . b₄ = (b₁ NormF ) . b₄ ) holds
b₃ is continuous

proof end;

theorem Th21: :: JGRAPH_4:21

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃ being Real
for b₄ being Subset of (TOP-REAL b₁) st b₄ = cl_Ball b₂,b₃ holds
( b₄ is Bounded & b₄ is closed )

proof end;

theorem Th22: :: JGRAPH_4:22

for b₁ being Point of (Euclid 2)
for b₂ being Real
for b₃ being Subset of (TOP-REAL 2) st b₃ = cl_Ball b₁,b₂ holds
b₃ is compact

proof end;

definition

let c₁ be real number ;
let c₂ be Point of (TOP-REAL 2);
func FanW c₁,c₂ -> Point of (TOP-REAL 2) equals :Def2: :: JGRAPH_4:def 2
|.a₂.| * |[(- (sqrt (1 - (((((a₂ `2 ) / |.a₂.|) - a₁) / (1 - a₁)) ^2 )))),((((a₂ `2 ) / |.a₂.|) - a₁) / (1 - a₁))]| if ( (a₂ `2 ) / |.a₂.| >= a₁ & a₂ `1 < 0 )
|.a₂.| * |[(- (sqrt (1 - (((((a₂ `2 ) / |.a₂.|) - a₁) / (1 + a₁)) ^2 )))),((((a₂ `2 ) / |.a₂.|) - a₁) / (1 + a₁))]| if ( (a₂ `2 ) / |.a₂.| < a₁ & a₂ `1 < 0 )
otherwise a₂;
correctness ;

end;

:: deftheorem Def2 defines FanW JGRAPH_4:def 2 :

definition

let c₁ be real number ;
func c₁ -FanMorphW -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def3: :: JGRAPH_4:def 3
for b₁ being Point of (TOP-REAL 2) holds a₂ . b₁ = FanW a₁,b₁;
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th23: :: JGRAPH_4:23

for b₁ being Point of (TOP-REAL 2)
for b₂ being real number holds
( ( (b₁ `2 ) / |.b₁.| >= b₂ & b₁ `1 < 0 implies (b₂ -FanMorphW ) . b₁ = |[(|.b₁.| * (- (sqrt (1 - (((((b₁ `2 ) / |.b₁.|) - b₂) / (1 - b₂)) ^2 ))))),(|.b₁.| * ((((b₁ `2 ) / |.b₁.|) - b₂) / (1 - b₂)))]| ) & ( b₁ `1 >= 0 implies (b₂ -FanMorphW ) . b₁ = b₁ ) )

proof end;

theorem Th24: :: JGRAPH_4:24

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real st (b₁ `2 ) / |.b₁.| <= b₂ & b₁ `1 < 0 holds
(b₂ -FanMorphW ) . b₁ = |[(|.b₁.| * (- (sqrt (1 - (((((b₁ `2 ) / |.b₁.|) - b₂) / (1 + b₂)) ^2 ))))),(|.b₁.| * ((((b₁ `2 ) / |.b₁.|) - b₂) / (1 + b₂)))]|

proof end;

theorem Th25: :: JGRAPH_4:25

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real st - 1 < b₂ & b₂ < 1 holds
( ( (b₁ `2 ) / |.b₁.| >= b₂ & b₁ `1 <= 0 & b₁ <> 0.REAL 2 implies (b₂ -FanMorphW ) . b₁ = |[(|.b₁.| * (- (sqrt (1 - (((((b₁ `2 ) / |.b₁.|) - b₂) / (1 - b₂)) ^2 ))))),(|.b₁.| * ((((b₁ `2 ) / |.b₁.|) - b₂) / (1 - b₂)))]| ) & ( (b₁ `2 ) / |.b₁.| <= b₂ & b₁ `1 <= 0 & b₁ <> 0.REAL 2 implies (b₂ -FanMorphW ) . b₁ = |[(|.b₁.| * (- (sqrt (1 - (((((b₁ `2 ) / |.b₁.|) - b₂) / (1 + b₂)) ^2 ))))),(|.b₁.| * ((((b₁ `2 ) / |.b₁.|) - b₂) / (1 + b₂)))]| ) )

proof end;

Lemma27: for b₁ being non empty Subset of (TOP-REAL 2) holds
( proj1 | b₁ is continuous Function of ((TOP-REAL 2) | b₁),R^1 & ( for b₂ being Point of ((TOP-REAL 2) | b₁) holds (proj1 | b₁) . b₂ = proj1 . b₂ ) )

proof end;

Lemma28: for b₁ being non empty Subset of (TOP-REAL 2) holds
( proj2 | b₁ is continuous Function of ((TOP-REAL 2) | b₁),R^1 & ( for b₂ being Point of ((TOP-REAL 2) | b₁) holds (proj2 | b₁) . b₂ = proj2 . b₂ ) )

proof end;

Lemma29: dom (2 NormF ) = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;

Lemma30: for b₁ being non empty Subset of (TOP-REAL 2) holds
( (2 NormF ) | b₁ is continuous Function of ((TOP-REAL 2) | b₁),R^1 & ( for b₂ being Point of ((TOP-REAL 2) | b₁) holds ((2 NormF ) | b₁) . b₂ = (2 NormF ) . b₂ ) )

proof end;

Lemma31: for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Function of ((TOP-REAL 2) | b₁),R^1 st b₂ = (2 NormF ) | b₁ & ( for b₃ being Point of (TOP-REAL 2) st b₃ in the carrier of ((TOP-REAL 2) | b₁) holds
b₃ <> 0.REAL 2 ) holds
for b₃ being Point of ((TOP-REAL 2) | b₁) holds b₂ . b₃ <> 0

proof end;

theorem Th26: :: JGRAPH_4:26

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * ((((b₄ `2 ) / |.b₄.|) - b₁) / (1 - b₁)) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `1 <= 0 & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th27: :: JGRAPH_4:27

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * ((((b₄ `2 ) / |.b₄.|) - b₁) / (1 + b₁)) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `1 <= 0 & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th28: :: JGRAPH_4:28

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * (- (sqrt (1 - (((((b₄ `2 ) / |.b₄.|) - b₁) / (1 - b₁)) ^2 )))) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `1 <= 0 & (b₄ `2 ) / |.b₄.| >= b₁ & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th29: :: JGRAPH_4:29

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * (- (sqrt (1 - (((((b₄ `2 ) / |.b₄.|) - b₁) / (1 + b₁)) ^2 )))) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `1 <= 0 & (b₄ `2 ) / |.b₄.| <= b₁ & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th30: :: JGRAPH_4:30

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphW ) | b₂ & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 <= 0 & b₅ <> 0.REAL 2 ) } & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( (b₅ `2 ) / |.b₅.| >= b₁ & b₅ `1 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th31: :: JGRAPH_4:31

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphW ) | b₂ & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 <= 0 & b₅ <> 0.REAL 2 ) } & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( (b₅ `2 ) / |.b₅.| <= b₁ & b₅ `1 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

Lemma38: for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 >= b₁ * |.b₃.| } holds
b₂ is closed

proof end;

Lemma39: for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `1 >= b₁ * |.b₃.| } holds
b₂ is closed

proof end;

theorem Th32: :: JGRAPH_4:32

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `2 >= b₁ * |.b₃.| & b₃ `1 <= 0 ) } holds
b₂ is closed

proof end;

Lemma41: for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 <= b₁ * |.b₃.| } holds
b₂ is closed

proof end;

Lemma42: for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `1 <= b₁ * |.b₃.| } holds
b₂ is closed

proof end;

theorem Th33: :: JGRAPH_4:33

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `2 <= b₁ * |.b₃.| & b₃ `1 <= 0 ) } holds
b₂ is closed

proof end;

theorem Th34: :: JGRAPH_4:34

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphW ) | b₂ & b₃ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th35: :: JGRAPH_4:35

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphW ) | b₂ & b₃ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th36: :: JGRAPH_4:36

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Subset of ((TOP-REAL 2) | b₁) st b₁ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `1 <= 0 & b₃ <> 0.REAL 2 ) } holds
b₂ is closed

proof end;

theorem Th37: :: JGRAPH_4:37

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Subset of ((TOP-REAL 2) | b₂)
for b₄ being Function of (((TOP-REAL 2) | b₂) | b₃),((TOP-REAL 2) | b₂) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphW ) | b₃ & b₂ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th38: :: JGRAPH_4:38

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Subset of ((TOP-REAL 2) | b₁) st b₁ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `1 >= 0 & b₃ <> 0.REAL 2 ) } holds
b₂ is closed

proof end;

theorem Th39: :: JGRAPH_4:39

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Subset of ((TOP-REAL 2) | b₂)
for b₄ being Function of (((TOP-REAL 2) | b₂) | b₃),((TOP-REAL 2) | b₂) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphW ) | b₃ & b₂ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th40: :: JGRAPH_4:40

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) holds |.((b₁ -FanMorphW ) . b₂).| = |.b₂.|

proof end;

theorem Th41: :: JGRAPH_4:41

for b₁ being Real
for b₂, b₃ being set st - 1 < b₁ & b₁ < 1 & b₂ in b₃ & b₃ = { b₄ where B is Point of (TOP-REAL 2) : ( b₄ `1 <= 0 & b₄ <> 0.REAL 2 ) } holds
(b₁ -FanMorphW ) . b₂ in b₃

proof end;

theorem Th42: :: JGRAPH_4:42

for b₁ being Real
for b₂, b₃ being set st - 1 < b₁ & b₁ < 1 & b₂ in b₃ & b₃ = { b₄ where B is Point of (TOP-REAL 2) : ( b₄ `1 >= 0 & b₄ <> 0.REAL 2 ) } holds
(b₁ -FanMorphW ) . b₂ in b₃

proof end;

scheme :: JGRAPH_4:sch 1
s1{ F₁() -> non empty Subset of (TOP-REAL 2), P₁[ set ] } :

{ b₁ where B is Point of (TOP-REAL 2) : ( P₁[b₁] & b₁ <> 0.REAL 2 ) } c= the carrier of ((TOP-REAL 2) | F₁())

provided

E53: F₁() = the carrier of (TOP-REAL 2) \ {(0.REAL 2)}

proof end;

theorem Th43: :: JGRAPH_4:43

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ ` = {(0.REAL 2)} holds
ex b₃ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₂) st
( b₃ = (b₁ -FanMorphW ) | b₂ & b₃ is continuous )

proof end;

theorem Th44: :: JGRAPH_4:44

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
ex b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₂ = b₁ -FanMorphW & b₂ is continuous )

proof end;

theorem Th45: :: JGRAPH_4:45

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
b₁ -FanMorphW is one-to-one

proof end;

theorem Th46: :: JGRAPH_4:46

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
( b₁ -FanMorphW is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (b₁ -FanMorphW ) = the carrier of (TOP-REAL 2) )

proof end;

E57: now

let c₁ be Subset of (TOP-REAL 2);
let c₂, c₃, c₄ be Point of (TOP-REAL 2);
let c₅, c₆, c₇ be Point of (Euclid 2);
assume E58: c₆ in cl_Ball c₅,(|.c₄.| + 1) ;
assume E59: ( c₃ = c₇ & c₂ = c₆ & c₅ = 0.REAL 2 ) ;
assume E60: |.c₂.| = |.c₃.| ;

now

assume not c₃ in cl_Ball c₅,(|.c₄.| + 1) ;
then not dist c₅,c₇ <= |.c₄.| + 1 by E59, METRIC_1:13;
then |.((0.REAL 2) - c₃).| > |.c₄.| + 1 by E59, JGRAPH_1:45;
then |.((0.REAL 2) + (- c₃)).| > |.c₄.| + 1 by EUCLID:45;
then |.(- c₃).| > |.c₄.| + 1 by EUCLID:31;
then |.c₃.| > |.c₄.| + 1 by TOPRNS_1:27;
then |.(- c₂).| > |.c₄.| + 1 by E60, TOPRNS_1:27;
then |.((0.REAL 2) + (- c₂)).| > |.c₄.| + 1 by EUCLID:31;
then |.((0.REAL 2) - c₂).| > |.c₄.| + 1 by EUCLID:45;
then dist c₅,c₆ > |.c₄.| + 1 by E59, JGRAPH_1:45;
hence contradiction by E58, METRIC_1:13;

end;

hence c₃ in cl_Ball c₅,(|.c₄.| + 1) ;

end;

theorem Th47: :: JGRAPH_4:47

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 holds
ex b₃ being non empty compact Subset of (TOP-REAL 2) st
( b₃ = (b₁ -FanMorphW ) .: b₃ & ex b₄ being Subset of (TOP-REAL 2) st
( b₂ in b₄ & b₄ is open & b₄ c= b₃ & (b₁ -FanMorphW ) . b₂ in b₄ ) )

proof end;

theorem Th48: :: JGRAPH_4:48

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
ex b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₂ = b₁ -FanMorphW & b₂ is_homeomorphism )

proof end;

E59: now

let c₁ be Point of (TOP-REAL 2);
let c₂, c₃ be Real;
assume ((- ((c₃ / |.c₁.|) - c₂)) / (1 - c₂)) ^2 < 1 ^2 ;
then 1 - (((- ((c₃ / |.c₁.|) - c₂)) / (1 - c₂)) ^2 ) > 0 by XREAL_1:52;
then sqrt (1 - (((- ((c₃ / |.c₁.|) - c₂)) / (1 - c₂)) ^2 )) > 0 by SQUARE_1:93;
then sqrt (1 - (((- ((c₃ / |.c₁.|) - c₂)) ^2 ) / ((1 - c₂) ^2 ))) > 0 by SQUARE_1:69;
then sqrt (1 - ((((c₃ / |.c₁.|) - c₂) ^2 ) / ((1 - c₂) ^2 ))) > 0 ;
then sqrt (1 - ((((c₃ / |.c₁.|) - c₂) / (1 - c₂)) ^2 )) > 0 by SQUARE_1:69;
hence - (sqrt (1 - ((((c₃ / |.c₁.|) - c₂) / (1 - c₂)) ^2 ))) < - 0 by XREAL_1:26;

end;

theorem Th49: :: JGRAPH_4:49

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 < 0 & (b₂ `2 ) / |.b₂.| >= b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphW ) . b₂ holds
( b₃ `1 < 0 & b₃ `2 >= 0 )

proof end;

theorem Th50: :: JGRAPH_4:50

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 < 0 & (b₂ `2 ) / |.b₂.| < b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphW ) . b₂ holds
( b₃ `1 < 0 & b₃ `2 < 0 )

proof end;

theorem Th51: :: JGRAPH_4:51

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 < 0 & (b₂ `2 ) / |.b₂.| >= b₁ & b₃ `1 < 0 & (b₃ `2 ) / |.b₃.| >= b₁ & (b₂ `2 ) / |.b₂.| < (b₃ `2 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphW ) . b₂ & b₅ = (b₁ -FanMorphW ) . b₃ holds
(b₄ `2 ) / |.b₄.| < (b₅ `2 ) / |.b₅.|

proof end;

theorem Th52: :: JGRAPH_4:52

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 < 0 & (b₂ `2 ) / |.b₂.| < b₁ & b₃ `1 < 0 & (b₃ `2 ) / |.b₃.| < b₁ & (b₂ `2 ) / |.b₂.| < (b₃ `2 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphW ) . b₂ & b₅ = (b₁ -FanMorphW ) . b₃ holds
(b₄ `2 ) / |.b₄.| < (b₅ `2 ) / |.b₅.|

proof end;

theorem Th53: :: JGRAPH_4:53

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 < 0 & b₃ `1 < 0 & (b₂ `2 ) / |.b₂.| < (b₃ `2 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphW ) . b₂ & b₅ = (b₁ -FanMorphW ) . b₃ holds
(b₄ `2 ) / |.b₄.| < (b₅ `2 ) / |.b₅.|

proof end;

theorem Th54: :: JGRAPH_4:54

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 < 0 & (b₂ `2 ) / |.b₂.| = b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphW ) . b₂ holds
( b₃ `1 < 0 & b₃ `2 = 0 )

proof end;

theorem Th55: :: JGRAPH_4:55

for b₁ being real number holds 0.REAL 2 = (b₁ -FanMorphW ) . (0.REAL 2) by Th23, JGRAPH_2:11;

definition

let c₁ be real number ;
let c₂ be Point of (TOP-REAL 2);
func FanN c₁,c₂ -> Point of (TOP-REAL 2) equals :Def4: :: JGRAPH_4:def 4
|.a₂.| * |[((((a₂ `1 ) / |.a₂.|) - a₁) / (1 - a₁)),(sqrt (1 - (((((a₂ `1 ) / |.a₂.|) - a₁) / (1 - a₁)) ^2 )))]| if ( (a₂ `1 ) / |.a₂.| >= a₁ & a₂ `2 > 0 )
|.a₂.| * |[((((a₂ `1 ) / |.a₂.|) - a₁) / (1 + a₁)),(sqrt (1 - (((((a₂ `1 ) / |.a₂.|) - a₁) / (1 + a₁)) ^2 )))]| if ( (a₂ `1 ) / |.a₂.| < a₁ & a₂ `2 > 0 )
otherwise a₂;
correctness ;

end;

:: deftheorem Def4 defines FanN JGRAPH_4:def 4 :

definition

let c₁ be real number ;
func c₁ -FanMorphN -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def5: :: JGRAPH_4:def 5
for b₁ being Point of (TOP-REAL 2) holds a₂ . b₁ = FanN a₁,b₁;
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th56: :: JGRAPH_4:56

for b₁ being Point of (TOP-REAL 2)
for b₂ being real number holds
( ( (b₁ `1 ) / |.b₁.| >= b₂ & b₁ `2 > 0 implies (b₂ -FanMorphN ) . b₁ = |[(|.b₁.| * ((((b₁ `1 ) / |.b₁.|) - b₂) / (1 - b₂))),(|.b₁.| * (sqrt (1 - (((((b₁ `1 ) / |.b₁.|) - b₂) / (1 - b₂)) ^2 ))))]| ) & ( b₁ `2 <= 0 implies (b₂ -FanMorphN ) . b₁ = b₁ ) )

proof end;

theorem Th57: :: JGRAPH_4:57

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real st (b₁ `1 ) / |.b₁.| <= b₂ & b₁ `2 > 0 holds
(b₂ -FanMorphN ) . b₁ = |[(|.b₁.| * ((((b₁ `1 ) / |.b₁.|) - b₂) / (1 + b₂))),(|.b₁.| * (sqrt (1 - (((((b₁ `1 ) / |.b₁.|) - b₂) / (1 + b₂)) ^2 ))))]|

proof end;

theorem Th58: :: JGRAPH_4:58

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real st - 1 < b₂ & b₂ < 1 holds
( ( (b₁ `1 ) / |.b₁.| >= b₂ & b₁ `2 >= 0 & b₁ <> 0.REAL 2 implies (b₂ -FanMorphN ) . b₁ = |[(|.b₁.| * ((((b₁ `1 ) / |.b₁.|) - b₂) / (1 - b₂))),(|.b₁.| * (sqrt (1 - (((((b₁ `1 ) / |.b₁.|) - b₂) / (1 - b₂)) ^2 ))))]| ) & ( (b₁ `1 ) / |.b₁.| <= b₂ & b₁ `2 >= 0 & b₁ <> 0.REAL 2 implies (b₂ -FanMorphN ) . b₁ = |[(|.b₁.| * ((((b₁ `1 ) / |.b₁.|) - b₂) / (1 + b₂))),(|.b₁.| * (sqrt (1 - (((((b₁ `1 ) / |.b₁.|) - b₂) / (1 + b₂)) ^2 ))))]| ) )

proof end;

theorem Th59: :: JGRAPH_4:59

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * ((((b₄ `1 ) / |.b₄.|) - b₁) / (1 - b₁)) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `2 >= 0 & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th60: :: JGRAPH_4:60

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * ((((b₄ `1 ) / |.b₄.|) - b₁) / (1 + b₁)) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `2 >= 0 & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th61: :: JGRAPH_4:61

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * (sqrt (1 - (((((b₄ `1 ) / |.b₄.|) - b₁) / (1 - b₁)) ^2 ))) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `2 >= 0 & (b₄ `1 ) / |.b₄.| >= b₁ & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th62: :: JGRAPH_4:62

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * (sqrt (1 - (((((b₄ `1 ) / |.b₄.|) - b₁) / (1 + b₁)) ^2 ))) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `2 >= 0 & (b₄ `1 ) / |.b₄.| <= b₁ & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th63: :: JGRAPH_4:63

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphN ) | b₂ & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 >= 0 & b₅ <> 0.REAL 2 ) } & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( (b₅ `1 ) / |.b₅.| >= b₁ & b₅ `2 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th64: :: JGRAPH_4:64

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphN ) | b₂ & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 >= 0 & b₅ <> 0.REAL 2 ) } & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( (b₅ `1 ) / |.b₅.| <= b₁ & b₅ `2 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th65: :: JGRAPH_4:65

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `1 >= b₁ * |.b₃.| & b₃ `2 >= 0 ) } holds
b₂ is closed

proof end;

theorem Th66: :: JGRAPH_4:66

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `1 <= b₁ * |.b₃.| & b₃ `2 >= 0 ) } holds
b₂ is closed

proof end;

theorem Th67: :: JGRAPH_4:67

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphN ) | b₂ & b₃ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th68: :: JGRAPH_4:68

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphN ) | b₂ & b₃ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th69: :: JGRAPH_4:69

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Subset of ((TOP-REAL 2) | b₁) st b₁ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `2 >= 0 & b₃ <> 0.REAL 2 ) } holds
b₂ is closed

proof end;

theorem Th70: :: JGRAPH_4:70

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Subset of ((TOP-REAL 2) | b₁) st b₁ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `2 <= 0 & b₃ <> 0.REAL 2 ) } holds
b₂ is closed

proof end;

theorem Th71: :: JGRAPH_4:71

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Subset of ((TOP-REAL 2) | b₂)
for b₄ being Function of (((TOP-REAL 2) | b₂) | b₃),((TOP-REAL 2) | b₂) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphN ) | b₃ & b₂ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th72: :: JGRAPH_4:72

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Subset of ((TOP-REAL 2) | b₂)
for b₄ being Function of (((TOP-REAL 2) | b₂) | b₃),((TOP-REAL 2) | b₂) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphN ) | b₃ & b₂ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th73: :: JGRAPH_4:73

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) holds |.((b₁ -FanMorphN ) . b₂).| = |.b₂.|

proof end;

theorem Th74: :: JGRAPH_4:74

for b₁ being Real
for b₂, b₃ being set st - 1 < b₁ & b₁ < 1 & b₂ in b₃ & b₃ = { b₄ where B is Point of (TOP-REAL 2) : ( b₄ `2 >= 0 & b₄ <> 0.REAL 2 ) } holds
(b₁ -FanMorphN ) . b₂ in b₃

proof end;

theorem Th75: :: JGRAPH_4:75

for b₁ being Real
for b₂, b₃ being set st - 1 < b₁ & b₁ < 1 & b₂ in b₃ & b₃ = { b₄ where B is Point of (TOP-REAL 2) : ( b₄ `2 <= 0 & b₄ <> 0.REAL 2 ) } holds
(b₁ -FanMorphN ) . b₂ in b₃

proof end;

theorem Th76: :: JGRAPH_4:76

proof end;

theorem Th77: :: JGRAPH_4:77

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
ex b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₂ = b₁ -FanMorphN & b₂ is continuous )

proof end;

theorem Th78: :: JGRAPH_4:78

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
b₁ -FanMorphN is one-to-one

proof end;

theorem Th79: :: JGRAPH_4:79

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
( b₁ -FanMorphN is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (b₁ -FanMorphN ) = the carrier of (TOP-REAL 2) )

proof end;

theorem Th80: :: JGRAPH_4:80

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 holds
ex b₃ being non empty compact Subset of (TOP-REAL 2) st
( b₃ = (b₁ -FanMorphN ) .: b₃ & ex b₄ being Subset of (TOP-REAL 2) st
( b₂ in b₄ & b₄ is open & b₄ c= b₃ & (b₁ -FanMorphN ) . b₂ in b₄ ) )

proof end;

theorem Th81: :: JGRAPH_4:81

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
ex b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₂ = b₁ -FanMorphN & b₂ is_homeomorphism )

proof end;

theorem Th82: :: JGRAPH_4:82

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 > 0 & (b₂ `1 ) / |.b₂.| >= b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphN ) . b₂ holds
( b₃ `2 > 0 & b₃ `1 >= 0 )

proof end;

theorem Th83: :: JGRAPH_4:83

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 > 0 & (b₂ `1 ) / |.b₂.| < b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphN ) . b₂ holds
( b₃ `2 > 0 & b₃ `1 < 0 )

proof end;

theorem Th84: :: JGRAPH_4:84

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 > 0 & (b₂ `1 ) / |.b₂.| >= b₁ & b₃ `2 > 0 & (b₃ `1 ) / |.b₃.| >= b₁ & (b₂ `1 ) / |.b₂.| < (b₃ `1 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphN ) . b₂ & b₅ = (b₁ -FanMorphN ) . b₃ holds
(b₄ `1 ) / |.b₄.| < (b₅ `1 ) / |.b₅.|

proof end;

theorem Th85: :: JGRAPH_4:85

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 > 0 & (b₂ `1 ) / |.b₂.| < b₁ & b₃ `2 > 0 & (b₃ `1 ) / |.b₃.| < b₁ & (b₂ `1 ) / |.b₂.| < (b₃ `1 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphN ) . b₂ & b₅ = (b₁ -FanMorphN ) . b₃ holds
(b₄ `1 ) / |.b₄.| < (b₅ `1 ) / |.b₅.|

proof end;

theorem Th86: :: JGRAPH_4:86

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 > 0 & b₃ `2 > 0 & (b₂ `1 ) / |.b₂.| < (b₃ `1 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphN ) . b₂ & b₅ = (b₁ -FanMorphN ) . b₃ holds
(b₄ `1 ) / |.b₄.| < (b₅ `1 ) / |.b₅.|

proof end;

theorem Th87: :: JGRAPH_4:87

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 > 0 & (b₂ `1 ) / |.b₂.| = b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphN ) . b₂ holds
( b₃ `2 > 0 & b₃ `1 = 0 )

proof end;

theorem Th88: :: JGRAPH_4:88

for b₁ being real number holds 0.REAL 2 = (b₁ -FanMorphN ) . (0.REAL 2) by Th56, JGRAPH_2:11;

definition

let c₁ be real number ;
let c₂ be Point of (TOP-REAL 2);
func FanE c₁,c₂ -> Point of (TOP-REAL 2) equals :Def6: :: JGRAPH_4:def 6
|.a₂.| * |[(sqrt (1 - (((((a₂ `2 ) / |.a₂.|) - a₁) / (1 - a₁)) ^2 ))),((((a₂ `2 ) / |.a₂.|) - a₁) / (1 - a₁))]| if ( (a₂ `2 ) / |.a₂.| >= a₁ & a₂ `1 > 0 )
|.a₂.| * |[(sqrt (1 - (((((a₂ `2 ) / |.a₂.|) - a₁) / (1 + a₁)) ^2 ))),((((a₂ `2 ) / |.a₂.|) - a₁) / (1 + a₁))]| if ( (a₂ `2 ) / |.a₂.| < a₁ & a₂ `1 > 0 )
otherwise a₂;
correctness ;

end;

:: deftheorem Def6 defines FanE JGRAPH_4:def 6 :

definition

let c₁ be real number ;
func c₁ -FanMorphE -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def7: :: JGRAPH_4:def 7
for b₁ being Point of (TOP-REAL 2) holds a₂ . b₁ = FanE a₁,b₁;
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th89: :: JGRAPH_4:89

for b₁ being Point of (TOP-REAL 2)
for b₂ being real number holds
( ( (b₁ `2 ) / |.b₁.| >= b₂ & b₁ `1 > 0 implies (b₂ -FanMorphE ) . b₁ = |[(|.b₁.| * (sqrt (1 - (((((b₁ `2 ) / |.b₁.|) - b₂) / (1 - b₂)) ^2 )))),(|.b₁.| * ((((b₁ `2 ) / |.b₁.|) - b₂) / (1 - b₂)))]| ) & ( b₁ `1 <= 0 implies (b₂ -FanMorphE ) . b₁ = b₁ ) )

proof end;

theorem Th90: :: JGRAPH_4:90

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real st (b₁ `2 ) / |.b₁.| <= b₂ & b₁ `1 > 0 holds
(b₂ -FanMorphE ) . b₁ = |[(|.b₁.| * (sqrt (1 - (((((b₁ `2 ) / |.b₁.|) - b₂) / (1 + b₂)) ^2 )))),(|.b₁.| * ((((b₁ `2 ) / |.b₁.|) - b₂) / (1 + b₂)))]|

proof end;

theorem Th91: :: JGRAPH_4:91

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real st - 1 < b₂ & b₂ < 1 holds
( ( (b₁ `2 ) / |.b₁.| >= b₂ & b₁ `1 >= 0 & b₁ <> 0.REAL 2 implies (b₂ -FanMorphE ) . b₁ = |[(|.b₁.| * (sqrt (1 - (((((b₁ `2 ) / |.b₁.|) - b₂) / (1 - b₂)) ^2 )))),(|.b₁.| * ((((b₁ `2 ) / |.b₁.|) - b₂) / (1 - b₂)))]| ) & ( (b₁ `2 ) / |.b₁.| <= b₂ & b₁ `1 >= 0 & b₁ <> 0.REAL 2 implies (b₂ -FanMorphE ) . b₁ = |[(|.b₁.| * (sqrt (1 - (((((b₁ `2 ) / |.b₁.|) - b₂) / (1 + b₂)) ^2 )))),(|.b₁.| * ((((b₁ `2 ) / |.b₁.|) - b₂) / (1 + b₂)))]| ) )

proof end;

theorem Th92: :: JGRAPH_4:92

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * ((((b₄ `2 ) / |.b₄.|) - b₁) / (1 - b₁)) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `1 >= 0 & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th93: :: JGRAPH_4:93

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * ((((b₄ `2 ) / |.b₄.|) - b₁) / (1 + b₁)) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `1 >= 0 & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th94: :: JGRAPH_4:94

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * (sqrt (1 - (((((b₄ `2 ) / |.b₄.|) - b₁) / (1 - b₁)) ^2 ))) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `1 >= 0 & (b₄ `2 ) / |.b₄.| >= b₁ & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th95: :: JGRAPH_4:95

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * (sqrt (1 - (((((b₄ `2 ) / |.b₄.|) - b₁) / (1 + b₁)) ^2 ))) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `1 >= 0 & (b₄ `2 ) / |.b₄.| <= b₁ & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th96: :: JGRAPH_4:96

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphE ) | b₂ & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 >= 0 & b₅ <> 0.REAL 2 ) } & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( (b₅ `2 ) / |.b₅.| >= b₁ & b₅ `1 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th97: :: JGRAPH_4:97

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphE ) | b₂ & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 >= 0 & b₅ <> 0.REAL 2 ) } & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( (b₅ `2 ) / |.b₅.| <= b₁ & b₅ `1 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th98: :: JGRAPH_4:98

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `2 >= b₁ * |.b₃.| & b₃ `1 >= 0 ) } holds
b₂ is closed

proof end;

theorem Th99: :: JGRAPH_4:99

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `2 <= b₁ * |.b₃.| & b₃ `1 >= 0 ) } holds
b₂ is closed

proof end;

theorem Th100: :: JGRAPH_4:100

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphE ) | b₂ & b₃ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th101: :: JGRAPH_4:101

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphE ) | b₂ & b₃ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th102: :: JGRAPH_4:102

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Subset of ((TOP-REAL 2) | b₂)
for b₄ being Function of (((TOP-REAL 2) | b₂) | b₃),((TOP-REAL 2) | b₂) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphE ) | b₃ & b₂ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th103: :: JGRAPH_4:103

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Subset of ((TOP-REAL 2) | b₂)
for b₄ being Function of (((TOP-REAL 2) | b₂) | b₃),((TOP-REAL 2) | b₂) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphE ) | b₃ & b₂ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th104: :: JGRAPH_4:104

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) holds |.((b₁ -FanMorphE ) . b₂).| = |.b₂.|

proof end;

theorem Th105: :: JGRAPH_4:105

for b₁ being Real
for b₂, b₃ being set st - 1 < b₁ & b₁ < 1 & b₂ in b₃ & b₃ = { b₄ where B is Point of (TOP-REAL 2) : ( b₄ `1 >= 0 & b₄ <> 0.REAL 2 ) } holds
(b₁ -FanMorphE ) . b₂ in b₃

proof end;

theorem Th106: :: JGRAPH_4:106

for b₁ being Real
for b₂, b₃ being set st - 1 < b₁ & b₁ < 1 & b₂ in b₃ & b₃ = { b₄ where B is Point of (TOP-REAL 2) : ( b₄ `1 <= 0 & b₄ <> 0.REAL 2 ) } holds
(b₁ -FanMorphE ) . b₂ in b₃

proof end;

theorem Th107: :: JGRAPH_4:107

proof end;

theorem Th108: :: JGRAPH_4:108

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
ex b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₂ = b₁ -FanMorphE & b₂ is continuous )

proof end;

theorem Th109: :: JGRAPH_4:109

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
b₁ -FanMorphE is one-to-one

proof end;

theorem Th110: :: JGRAPH_4:110

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
( b₁ -FanMorphE is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (b₁ -FanMorphE ) = the carrier of (TOP-REAL 2) )

proof end;

theorem Th111: :: JGRAPH_4:111

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 holds
ex b₃ being non empty compact Subset of (TOP-REAL 2) st
( b₃ = (b₁ -FanMorphE ) .: b₃ & ex b₄ being Subset of (TOP-REAL 2) st
( b₂ in b₄ & b₄ is open & b₄ c= b₃ & (b₁ -FanMorphE ) . b₂ in b₄ ) )

proof end;

theorem Th112: :: JGRAPH_4:112

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
ex b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₂ = b₁ -FanMorphE & b₂ is_homeomorphism )

proof end;

theorem Th113: :: JGRAPH_4:113

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 > 0 & (b₂ `2 ) / |.b₂.| >= b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphE ) . b₂ holds
( b₃ `1 > 0 & b₃ `2 >= 0 )

proof end;

theorem Th114: :: JGRAPH_4:114

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 > 0 & (b₂ `2 ) / |.b₂.| < b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphE ) . b₂ holds
( b₃ `1 > 0 & b₃ `2 < 0 )

proof end;

theorem Th115: :: JGRAPH_4:115

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 > 0 & (b₂ `2 ) / |.b₂.| >= b₁ & b₃ `1 > 0 & (b₃ `2 ) / |.b₃.| >= b₁ & (b₂ `2 ) / |.b₂.| < (b₃ `2 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphE ) . b₂ & b₅ = (b₁ -FanMorphE ) . b₃ holds
(b₄ `2 ) / |.b₄.| < (b₅ `2 ) / |.b₅.|

proof end;

theorem Th116: :: JGRAPH_4:116

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 > 0 & (b₂ `2 ) / |.b₂.| < b₁ & b₃ `1 > 0 & (b₃ `2 ) / |.b₃.| < b₁ & (b₂ `2 ) / |.b₂.| < (b₃ `2 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphE ) . b₂ & b₅ = (b₁ -FanMorphE ) . b₃ holds
(b₄ `2 ) / |.b₄.| < (b₅ `2 ) / |.b₅.|

proof end;

theorem Th117: :: JGRAPH_4:117

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 > 0 & b₃ `1 > 0 & (b₂ `2 ) / |.b₂.| < (b₃ `2 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphE ) . b₂ & b₅ = (b₁ -FanMorphE ) . b₃ holds
(b₄ `2 ) / |.b₄.| < (b₅ `2 ) / |.b₅.|

proof end;

theorem Th118: :: JGRAPH_4:118

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 > 0 & (b₂ `2 ) / |.b₂.| = b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphE ) . b₂ holds
( b₃ `1 > 0 & b₃ `2 = 0 )

proof end;

theorem Th119: :: JGRAPH_4:119

for b₁ being real number holds 0.REAL 2 = (b₁ -FanMorphE ) . (0.REAL 2) by Th89, JGRAPH_2:11;

definition

let c₁ be real number ;
let c₂ be Point of (TOP-REAL 2);
func FanS c₁,c₂ -> Point of (TOP-REAL 2) equals :Def8: :: JGRAPH_4:def 8
|.a₂.| * |[((((a₂ `1 ) / |.a₂.|) - a₁) / (1 - a₁)),(- (sqrt (1 - (((((a₂ `1 ) / |.a₂.|) - a₁) / (1 - a₁)) ^2 ))))]| if ( (a₂ `1 ) / |.a₂.| >= a₁ & a₂ `2 < 0 )
|.a₂.| * |[((((a₂ `1 ) / |.a₂.|) - a₁) / (1 + a₁)),(- (sqrt (1 - (((((a₂ `1 ) / |.a₂.|) - a₁) / (1 + a₁)) ^2 ))))]| if ( (a₂ `1 ) / |.a₂.| < a₁ & a₂ `2 < 0 )
otherwise a₂;
correctness ;

end;

:: deftheorem Def8 defines FanS JGRAPH_4:def 8 :

definition

let c₁ be real number ;
func c₁ -FanMorphS -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def9: :: JGRAPH_4:def 9
for b₁ being Point of (TOP-REAL 2) holds a₂ . b₁ = FanS a₁,b₁;
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th120: :: JGRAPH_4:120

for b₁ being Point of (TOP-REAL 2)
for b₂ being real number holds
( ( (b₁ `1 ) / |.b₁.| >= b₂ & b₁ `2 < 0 implies (b₂ -FanMorphS ) . b₁ = |[(|.b₁.| * ((((b₁ `1 ) / |.b₁.|) - b₂) / (1 - b₂))),(|.b₁.| * (- (sqrt (1 - (((((b₁ `1 ) / |.b₁.|) - b₂) / (1 - b₂)) ^2 )))))]| ) & ( b₁ `2 >= 0 implies (b₂ -FanMorphS ) . b₁ = b₁ ) )

proof end;

theorem Th121: :: JGRAPH_4:121

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real st (b₁ `1 ) / |.b₁.| <= b₂ & b₁ `2 < 0 holds
(b₂ -FanMorphS ) . b₁ = |[(|.b₁.| * ((((b₁ `1 ) / |.b₁.|) - b₂) / (1 + b₂))),(|.b₁.| * (- (sqrt (1 - (((((b₁ `1 ) / |.b₁.|) - b₂) / (1 + b₂)) ^2 )))))]|

proof end;

theorem Th122: :: JGRAPH_4:122

for b₁ being Point of (TOP-REAL 2)
for b₂ being Real st - 1 < b₂ & b₂ < 1 holds
( ( (b₁ `1 ) / |.b₁.| >= b₂ & b₁ `2 <= 0 & b₁ <> 0.REAL 2 implies (b₂ -FanMorphS ) . b₁ = |[(|.b₁.| * ((((b₁ `1 ) / |.b₁.|) - b₂) / (1 - b₂))),(|.b₁.| * (- (sqrt (1 - (((((b₁ `1 ) / |.b₁.|) - b₂) / (1 - b₂)) ^2 )))))]| ) & ( (b₁ `1 ) / |.b₁.| <= b₂ & b₁ `2 <= 0 & b₁ <> 0.REAL 2 implies (b₂ -FanMorphS ) . b₁ = |[(|.b₁.| * ((((b₁ `1 ) / |.b₁.|) - b₂) / (1 + b₂))),(|.b₁.| * (- (sqrt (1 - (((((b₁ `1 ) / |.b₁.|) - b₂) / (1 + b₂)) ^2 )))))]| ) )

proof end;

theorem Th123: :: JGRAPH_4:123

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * ((((b₄ `1 ) / |.b₄.|) - b₁) / (1 - b₁)) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `2 <= 0 & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th124: :: JGRAPH_4:124

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * ((((b₄ `1 ) / |.b₄.|) - b₁) / (1 + b₁)) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `2 <= 0 & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th125: :: JGRAPH_4:125

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * (- (sqrt (1 - (((((b₄ `1 ) / |.b₄.|) - b₁) / (1 - b₁)) ^2 )))) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `2 <= 0 & (b₄ `1 ) / |.b₄.| >= b₁ & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th126: :: JGRAPH_4:126

for b₁ being Real
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₂),R^1 st - 1 < b₁ & b₁ < 1 & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
b₃ . b₄ = |.b₄.| * (- (sqrt (1 - (((((b₄ `1 ) / |.b₄.|) - b₁) / (1 + b₁)) ^2 )))) ) & ( for b₄ being Point of (TOP-REAL 2) st b₄ in the carrier of ((TOP-REAL 2) | b₂) holds
( b₄ `2 <= 0 & (b₄ `1 ) / |.b₄.| <= b₁ & b₄ <> 0.REAL 2 ) ) holds
b₃ is continuous

proof end;

theorem Th127: :: JGRAPH_4:127

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphS ) | b₂ & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 <= 0 & b₅ <> 0.REAL 2 ) } & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( (b₅ `1 ) / |.b₅.| >= b₁ & b₅ `2 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th128: :: JGRAPH_4:128

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphS ) | b₂ & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 <= 0 & b₅ <> 0.REAL 2 ) } & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( (b₅ `1 ) / |.b₅.| <= b₁ & b₅ `2 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th129: :: JGRAPH_4:129

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `1 >= b₁ * |.b₃.| & b₃ `2 <= 0 ) } holds
b₂ is closed

proof end;

theorem Th130: :: JGRAPH_4:130

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2) st b₂ = { b₃ where B is Point of (TOP-REAL 2) : ( b₃ `1 <= b₁ * |.b₃.| & b₃ `2 <= 0 ) } holds
b₂ is closed

proof end;

theorem Th131: :: JGRAPH_4:131

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphS ) | b₂ & b₃ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th132: :: JGRAPH_4:132

for b₁ being Real
for b₂, b₃ being Subset of (TOP-REAL 2)
for b₄ being Function of ((TOP-REAL 2) | b₂),((TOP-REAL 2) | b₃) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphS ) | b₂ & b₃ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₂ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th133: :: JGRAPH_4:133

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Subset of ((TOP-REAL 2) | b₂)
for b₄ being Function of (((TOP-REAL 2) | b₂) | b₃),((TOP-REAL 2) | b₂) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphS ) | b₃ & b₂ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 <= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th134: :: JGRAPH_4:134

for b₁ being Real
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Subset of ((TOP-REAL 2) | b₂)
for b₄ being Function of (((TOP-REAL 2) | b₂) | b₃),((TOP-REAL 2) | b₂) st - 1 < b₁ & b₁ < 1 & b₄ = (b₁ -FanMorphS ) | b₃ & b₂ = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b₃ = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `2 >= 0 & b₅ <> 0.REAL 2 ) } holds
b₄ is continuous

proof end;

theorem Th135: :: JGRAPH_4:135

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) holds |.((b₁ -FanMorphS ) . b₂).| = |.b₂.|

proof end;

theorem Th136: :: JGRAPH_4:136

for b₁ being Real
for b₂, b₃ being set st - 1 < b₁ & b₁ < 1 & b₂ in b₃ & b₃ = { b₄ where B is Point of (TOP-REAL 2) : ( b₄ `2 <= 0 & b₄ <> 0.REAL 2 ) } holds
(b₁ -FanMorphS ) . b₂ in b₃

proof end;

theorem Th137: :: JGRAPH_4:137

for b₁ being Real
for b₂, b₃ being set st - 1 < b₁ & b₁ < 1 & b₂ in b₃ & b₃ = { b₄ where B is Point of (TOP-REAL 2) : ( b₄ `2 >= 0 & b₄ <> 0.REAL 2 ) } holds
(b₁ -FanMorphS ) . b₂ in b₃

proof end;

theorem Th138: :: JGRAPH_4:138

proof end;

theorem Th139: :: JGRAPH_4:139

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
ex b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₂ = b₁ -FanMorphS & b₂ is continuous )

proof end;

theorem Th140: :: JGRAPH_4:140

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
b₁ -FanMorphS is one-to-one

proof end;

theorem Th141: :: JGRAPH_4:141

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
( b₁ -FanMorphS is Function of (TOP-REAL 2),(TOP-REAL 2) & rng (b₁ -FanMorphS ) = the carrier of (TOP-REAL 2) )

proof end;

theorem Th142: :: JGRAPH_4:142

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 holds
ex b₃ being non empty compact Subset of (TOP-REAL 2) st
( b₃ = (b₁ -FanMorphS ) .: b₃ & ex b₄ being Subset of (TOP-REAL 2) st
( b₂ in b₄ & b₄ is open & b₄ c= b₃ & (b₁ -FanMorphS ) . b₂ in b₄ ) )

proof end;

theorem Th143: :: JGRAPH_4:143

for b₁ being Real st - 1 < b₁ & b₁ < 1 holds
ex b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₂ = b₁ -FanMorphS & b₂ is_homeomorphism )

proof end;

theorem Th144: :: JGRAPH_4:144

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 < 0 & (b₂ `1 ) / |.b₂.| >= b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphS ) . b₂ holds
( b₃ `2 < 0 & b₃ `1 >= 0 )

proof end;

theorem Th145: :: JGRAPH_4:145

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 < 0 & (b₂ `1 ) / |.b₂.| < b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphS ) . b₂ holds
( b₃ `2 < 0 & b₃ `1 < 0 )

proof end;

theorem Th146: :: JGRAPH_4:146

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 < 0 & (b₂ `1 ) / |.b₂.| >= b₁ & b₃ `2 < 0 & (b₃ `1 ) / |.b₃.| >= b₁ & (b₂ `1 ) / |.b₂.| < (b₃ `1 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphS ) . b₂ & b₅ = (b₁ -FanMorphS ) . b₃ holds
(b₄ `1 ) / |.b₄.| < (b₅ `1 ) / |.b₅.|

proof end;

theorem Th147: :: JGRAPH_4:147

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 < 0 & (b₂ `1 ) / |.b₂.| < b₁ & b₃ `2 < 0 & (b₃ `1 ) / |.b₃.| < b₁ & (b₂ `1 ) / |.b₂.| < (b₃ `1 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphS ) . b₂ & b₅ = (b₁ -FanMorphS ) . b₃ holds
(b₄ `1 ) / |.b₄.| < (b₅ `1 ) / |.b₅.|

proof end;

theorem Th148: :: JGRAPH_4:148

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 < 0 & b₃ `2 < 0 & (b₂ `1 ) / |.b₂.| < (b₃ `1 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphS ) . b₂ & b₅ = (b₁ -FanMorphS ) . b₃ holds
(b₄ `1 ) / |.b₄.| < (b₅ `1 ) / |.b₅.|

proof end;

theorem Th149: :: JGRAPH_4:149

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 < 0 & (b₂ `1 ) / |.b₂.| = b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphS ) . b₂ holds
( b₃ `2 < 0 & b₃ `1 = 0 )

proof end;

theorem Th150: :: JGRAPH_4:150

for b₁ being real number holds 0.REAL 2 = (b₁ -FanMorphS ) . (0.REAL 2) by Th120, JGRAPH_2:11;