:: by Yatsuka Nakamura

::

:: Received June 24, 2002

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

theorem Th1: :: JGRAPH_5:1

for p being Point of (TOP-REAL 2) st |.p.| <= 1 holds

( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 )

( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 )

proof end;

theorem Th2: :: JGRAPH_5:2

for p being Point of (TOP-REAL 2) st |.p.| <= 1 & p `1 <> 0 & p `2 <> 0 holds

( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 )

( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 )

proof end;

theorem :: JGRAPH_5:3

for a, b, d, e, r3 being Real

for PM, PM2 being non empty MetrStruct

for x being Element of PM

for x2 being Element of PM2 st d <= a & a <= b & b <= e & PM = Closed-Interval-MSpace (a,b) & PM2 = Closed-Interval-MSpace (d,e) & x = x2 holds

Ball (x,r3) c= Ball (x2,r3)

for PM, PM2 being non empty MetrStruct

for x being Element of PM

for x2 being Element of PM2 st d <= a & a <= b & b <= e & PM = Closed-Interval-MSpace (a,b) & PM2 = Closed-Interval-MSpace (d,e) & x = x2 holds

Ball (x,r3) c= Ball (x2,r3)

proof end;

theorem :: JGRAPH_5:4

theorem Th5: :: JGRAPH_5:5

for X being TopStruct

for Y, Z being non empty TopStruct

for f being Function of X,Y

for h being Function of Y,Z st h is being_homeomorphism & f is continuous holds

h * f is continuous

for Y, Z being non empty TopStruct

for f being Function of X,Y

for h being Function of Y,Z st h is being_homeomorphism & f is continuous holds

h * f is continuous

proof end;

theorem Th6: :: JGRAPH_5:6

for X, Y, Z being TopStruct

for f being Function of X,Y

for h being Function of Y,Z st h is being_homeomorphism & f is one-to-one holds

h * f is one-to-one

for f being Function of X,Y

for h being Function of Y,Z st h is being_homeomorphism & f is one-to-one holds

h * f is one-to-one

proof end;

theorem Th7: :: JGRAPH_5:7

for X being TopStruct

for S, V being non empty TopStruct

for B being non empty Subset of S

for f being Function of X,(S | B)

for g being Function of S,V

for h being Function of X,V st h = g * f & f is continuous & g is continuous holds

h is continuous

for S, V being non empty TopStruct

for B being non empty Subset of S

for f being Function of X,(S | B)

for g being Function of S,V

for h being Function of X,V st h = g * f & f is continuous & g is continuous holds

h is continuous

proof end;

theorem Th8: :: JGRAPH_5:8

for a, b, d, e, s1, s2, t1, t2 being Real

for h being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (d,e)) st h is being_homeomorphism & h . s1 = t1 & h . s2 = t2 & h . b = e & d <= e & t1 <= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds

s1 <= s2

for h being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (d,e)) st h is being_homeomorphism & h . s1 = t1 & h . s2 = t2 & h . b = e & d <= e & t1 <= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds

s1 <= s2

proof end;

theorem Th9: :: JGRAPH_5:9

for a, b, d, e, s1, s2, t1, t2 being Real

for h being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (d,e)) st h is being_homeomorphism & h . s1 = t1 & h . s2 = t2 & h . b = d & e >= d & t1 >= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds

s1 <= s2

for h being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (d,e)) st h is being_homeomorphism & h . s1 = t1 & h . s2 = t2 & h . b = d & e >= d & t1 >= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds

s1 <= s2

proof end;

theorem Th11: :: JGRAPH_5:11

for f, g being Function of I[01],(TOP-REAL 2)

for a, b, c, d being Real

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & a <> b & c <> d & (f . O) `1 = a & c <= (f . O) `2 & (f . O) `2 <= d & (f . I) `1 = b & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & a <= (g . O) `1 & (g . O) `1 <= b & (g . I) `2 = d & a <= (g . I) `1 & (g . I) `1 <= b & ( for r being Point of I[01] holds

( ( a >= (f . r) `1 or (f . r) `1 >= b or c >= (f . r) `2 or (f . r) `2 >= d ) & ( a >= (g . r) `1 or (g . r) `1 >= b or c >= (g . r) `2 or (g . r) `2 >= d ) ) ) holds

rng f meets rng g

for a, b, c, d being Real

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & a <> b & c <> d & (f . O) `1 = a & c <= (f . O) `2 & (f . O) `2 <= d & (f . I) `1 = b & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & a <= (g . O) `1 & (g . O) `1 <= b & (g . I) `2 = d & a <= (g . I) `1 & (g . I) `1 <= b & ( for r being Point of I[01] holds

( ( a >= (f . r) `1 or (f . r) `1 >= b or c >= (f . r) `2 or (f . r) `2 >= d ) & ( a >= (g . r) `1 or (g . r) `1 >= b or c >= (g . r) `2 or (g . r) `2 >= d ) ) ) holds

rng f meets rng g

proof end;

Lm1: 0 in [.0,1.]

by XXREAL_1:1;

Lm2: 1 in [.0,1.]

by XXREAL_1:1;

theorem Th12: :: JGRAPH_5:12

for f being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one holds

ex f2 being Function of I[01],(TOP-REAL 2) st

( f2 . 0 = f . 1 & f2 . 1 = f . 0 & rng f2 = rng f & f2 is continuous & f2 is one-to-one )

ex f2 being Function of I[01],(TOP-REAL 2) st

( f2 . 0 = f . 1 & f2 . 1 = f . 0 & rng f2 = rng f & f2 is continuous & f2 is one-to-one )

proof end;

theorem Th13: :: JGRAPH_5:13

for f, g being Function of I[01],(TOP-REAL 2)

for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYP & g . I in KYN & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYP & g . I in KYN & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;

theorem Th14: :: JGRAPH_5:14

for f, g being Function of I[01],(TOP-REAL 2)

for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;

theorem Th15: :: JGRAPH_5:15

for f, g being Function of I[01],(TOP-REAL 2)

for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYP & g . I in KYN & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYP & g . I in KYN & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;

theorem Th16: :: JGRAPH_5:16

for f, g being Function of I[01],(TOP-REAL 2)

for C0 being Subset of (TOP-REAL 2) st C0 = { q where q is Point of (TOP-REAL 2) : |.q.| >= 1 } & f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = |[(- 1),0]| & f . 1 = |[1,0]| & g . 1 = |[0,1]| & g . 0 = |[0,(- 1)]| & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

for C0 being Subset of (TOP-REAL 2) st C0 = { q where q is Point of (TOP-REAL 2) : |.q.| >= 1 } & f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = |[(- 1),0]| & f . 1 = |[1,0]| & g . 1 = |[0,1]| & g . 0 = |[0,(- 1)]| & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;

theorem :: JGRAPH_5:17

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for C0 being Subset of (TOP-REAL 2) st C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & |.p1.| = 1 & |.p2.| = 1 & |.p3.| = 1 & |.p4.| = 1 & ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st

( h is being_homeomorphism & h .: C0 c= C0 & h . p1 = |[(- 1),0]| & h . p2 = |[0,1]| & h . p3 = |[1,0]| & h . p4 = |[0,(- 1)]| ) holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

for C0 being Subset of (TOP-REAL 2) st C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & |.p1.| = 1 & |.p2.| = 1 & |.p3.| = 1 & |.p4.| = 1 & ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st

( h is being_homeomorphism & h .: C0 c= C0 & h . p1 = |[(- 1),0]| & h . p2 = |[0,1]| & h . p3 = |[1,0]| & h . p4 = |[0,(- 1)]| ) holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;

theorem Th18: :: JGRAPH_5:18

for cn being Real

for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 > 0 holds

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds

p `2 > 0

for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 > 0 holds

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds

p `2 > 0

proof end;

theorem :: JGRAPH_5:19

for cn being Real

for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 >= 0 holds

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds

p `2 >= 0

for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 >= 0 holds

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds

p `2 >= 0

proof end;

theorem Th20: :: JGRAPH_5:20

for cn being Real

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

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds

( p `2 >= 0 & p `1 < 0 )

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

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds

( p `2 >= 0 & p `1 < 0 )

proof end;

theorem Th21: :: JGRAPH_5:21

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.| <> 0 & |.q2.| <> 0 & (q1 `1) / |.q1.| < (q2 `1) / |.q2.| holds

for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphN) . q1 & p2 = (cn -FanMorphN) . q2 holds

(p1 `1) / |.p1.| < (p2 `1) / |.p2.|

for q1, q2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q1 `2 >= 0 & q2 `2 >= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `1) / |.q1.| < (q2 `1) / |.q2.| holds

for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphN) . q1 & p2 = (cn -FanMorphN) . q2 holds

(p1 `1) / |.p1.| < (p2 `1) / |.p2.|

proof end;

theorem Th22: :: JGRAPH_5:22

for sn being Real

for q being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 & q `1 > 0 holds

for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds

p `1 > 0

for q being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 & q `1 > 0 holds

for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds

p `1 > 0

proof end;

theorem :: JGRAPH_5:23

for sn being Real

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

for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds

( p `1 >= 0 & p `2 < 0 )

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

for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds

( p `1 >= 0 & p `2 < 0 )

proof end;

theorem Th24: :: JGRAPH_5:24

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.| <> 0 & |.q2.| <> 0 & (q1 `2) / |.q1.| < (q2 `2) / |.q2.| holds

for p1, p2 being Point of (TOP-REAL 2) st p1 = (sn -FanMorphE) . q1 & p2 = (sn -FanMorphE) . q2 holds

(p1 `2) / |.p1.| < (p2 `2) / |.p2.|

for q1, q2 being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 & q1 `1 >= 0 & q2 `1 >= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `2) / |.q1.| < (q2 `2) / |.q2.| holds

for p1, p2 being Point of (TOP-REAL 2) st p1 = (sn -FanMorphE) . q1 & p2 = (sn -FanMorphE) . q2 holds

(p1 `2) / |.p1.| < (p2 `2) / |.p2.|

proof end;

theorem Th25: :: JGRAPH_5:25

for cn being Real

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

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds

p `2 < 0

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

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds

p `2 < 0

proof end;

theorem Th26: :: JGRAPH_5:26

for cn being Real

for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 < 0 & (q `1) / |.q.| > cn holds

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds

( p `2 < 0 & p `1 > 0 )

for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 < 0 & (q `1) / |.q.| > cn holds

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds

( p `2 < 0 & p `1 > 0 )

proof end;

theorem Th27: :: JGRAPH_5:27

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.| <> 0 & |.q2.| <> 0 & (q1 `1) / |.q1.| < (q2 `1) / |.q2.| holds

for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS) . q1 & p2 = (cn -FanMorphS) . q2 holds

(p1 `1) / |.p1.| < (p2 `1) / |.p2.|

for q1, q2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q1 `2 <= 0 & q2 `2 <= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `1) / |.q1.| < (q2 `1) / |.q2.| holds

for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS) . q1 & p2 = (cn -FanMorphS) . q2 holds

(p1 `1) / |.p1.| < (p2 `1) / |.p2.|

proof end;

Lm3: now :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds

( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] )

( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] )

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } implies ( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] ) )

assume A1: P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ; :: thesis: ( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] )

A2: [.(- 1),1.] c= proj1 .: P

A12: [.(- 1),1.] c= proj2 .: P

end;
assume A1: P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ; :: thesis: ( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] )

A2: [.(- 1),1.] c= proj1 .: P

proof

proj1 .: P c= [.(- 1),1.]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [.(- 1),1.] or y in proj1 .: P )

assume y in [.(- 1),1.] ; :: thesis: y in proj1 .: P

then y in { r where r is Real : ( - 1 <= r & r <= 1 ) } by RCOMP_1:def 1;

then consider r being Real such that

A3: y = r and

A4: ( - 1 <= r & r <= 1 ) ;

set q = |[r,(sqrt (1 - (r ^2)))]|;

1 ^2 >= r ^2 by A4, SQUARE_1:49;

then A5: 1 - (r ^2) >= 0 by XREAL_1:48;

( |[r,(sqrt (1 - (r ^2)))]| `1 = r & |[r,(sqrt (1 - (r ^2)))]| `2 = sqrt (1 - (r ^2)) ) by EUCLID:52;

then |.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) by JGRAPH_3:1

.= sqrt ((r ^2) + (1 - (r ^2))) by A5, SQUARE_1:def 2

.= 1 by SQUARE_1:18 ;

then A6: ( dom proj1 = the carrier of (TOP-REAL 2) & |[r,(sqrt (1 - (r ^2)))]| in P ) by A1, FUNCT_2:def 1;

proj1 . |[r,(sqrt (1 - (r ^2)))]| = |[r,(sqrt (1 - (r ^2)))]| `1 by PSCOMP_1:def 5

.= r by EUCLID:52 ;

hence y in proj1 .: P by A3, A6, FUNCT_1:def 6; :: thesis: verum

end;
assume y in [.(- 1),1.] ; :: thesis: y in proj1 .: P

then y in { r where r is Real : ( - 1 <= r & r <= 1 ) } by RCOMP_1:def 1;

then consider r being Real such that

A3: y = r and

A4: ( - 1 <= r & r <= 1 ) ;

set q = |[r,(sqrt (1 - (r ^2)))]|;

1 ^2 >= r ^2 by A4, SQUARE_1:49;

then A5: 1 - (r ^2) >= 0 by XREAL_1:48;

( |[r,(sqrt (1 - (r ^2)))]| `1 = r & |[r,(sqrt (1 - (r ^2)))]| `2 = sqrt (1 - (r ^2)) ) by EUCLID:52;

then |.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) by JGRAPH_3:1

.= sqrt ((r ^2) + (1 - (r ^2))) by A5, SQUARE_1:def 2

.= 1 by SQUARE_1:18 ;

then A6: ( dom proj1 = the carrier of (TOP-REAL 2) & |[r,(sqrt (1 - (r ^2)))]| in P ) by A1, FUNCT_2:def 1;

proj1 . |[r,(sqrt (1 - (r ^2)))]| = |[r,(sqrt (1 - (r ^2)))]| `1 by PSCOMP_1:def 5

.= r by EUCLID:52 ;

hence y in proj1 .: P by A3, A6, FUNCT_1:def 6; :: thesis: verum

proof

hence
proj1 .: P = [.(- 1),1.]
by A2, XBOOLE_0:def 10; :: thesis: proj2 .: P = [.(- 1),1.]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj1 .: P or y in [.(- 1),1.] )

assume y in proj1 .: P ; :: thesis: y in [.(- 1),1.]

then consider x being object such that

A7: x in dom proj1 and

A8: x in P and

A9: y = proj1 . x by FUNCT_1:def 6;

reconsider q = x as Point of (TOP-REAL 2) by A7;

ex q2 being Point of (TOP-REAL 2) st

( q2 = x & |.q2.| = 1 ) by A1, A8;

then A10: ((q `1) ^2) + ((q `2) ^2) = 1 ^2 by JGRAPH_3:1;

0 <= (q `2) ^2 by XREAL_1:63;

then (1 - ((q `1) ^2)) + ((q `1) ^2) >= 0 + ((q `1) ^2) by A10, XREAL_1:7;

then A11: ( - 1 <= q `1 & q `1 <= 1 ) by SQUARE_1:51;

y = q `1 by A9, PSCOMP_1:def 5;

hence y in [.(- 1),1.] by A11, XXREAL_1:1; :: thesis: verum

end;
assume y in proj1 .: P ; :: thesis: y in [.(- 1),1.]

then consider x being object such that

A7: x in dom proj1 and

A8: x in P and

A9: y = proj1 . x by FUNCT_1:def 6;

reconsider q = x as Point of (TOP-REAL 2) by A7;

ex q2 being Point of (TOP-REAL 2) st

( q2 = x & |.q2.| = 1 ) by A1, A8;

then A10: ((q `1) ^2) + ((q `2) ^2) = 1 ^2 by JGRAPH_3:1;

0 <= (q `2) ^2 by XREAL_1:63;

then (1 - ((q `1) ^2)) + ((q `1) ^2) >= 0 + ((q `1) ^2) by A10, XREAL_1:7;

then A11: ( - 1 <= q `1 & q `1 <= 1 ) by SQUARE_1:51;

y = q `1 by A9, PSCOMP_1:def 5;

hence y in [.(- 1),1.] by A11, XXREAL_1:1; :: thesis: verum

A12: [.(- 1),1.] c= proj2 .: P

proof

proj2 .: P c= [.(- 1),1.]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [.(- 1),1.] or y in proj2 .: P )

assume y in [.(- 1),1.] ; :: thesis: y in proj2 .: P

then y in { r where r is Real : ( - 1 <= r & r <= 1 ) } by RCOMP_1:def 1;

then consider r being Real such that

A13: y = r and

A14: ( - 1 <= r & r <= 1 ) ;

set q = |[(sqrt (1 - (r ^2))),r]|;

1 ^2 >= r ^2 by A14, SQUARE_1:49;

then A15: 1 - (r ^2) >= 0 by XREAL_1:48;

( |[(sqrt (1 - (r ^2))),r]| `2 = r & |[(sqrt (1 - (r ^2))),r]| `1 = sqrt (1 - (r ^2)) ) by EUCLID:52;

then |.|[(sqrt (1 - (r ^2))),r]|.| = sqrt (((sqrt (1 - (r ^2))) ^2) + (r ^2)) by JGRAPH_3:1

.= sqrt ((1 - (r ^2)) + (r ^2)) by A15, SQUARE_1:def 2

.= 1 by SQUARE_1:18 ;

then A16: ( dom proj2 = the carrier of (TOP-REAL 2) & |[(sqrt (1 - (r ^2))),r]| in P ) by A1, FUNCT_2:def 1;

proj2 . |[(sqrt (1 - (r ^2))),r]| = |[(sqrt (1 - (r ^2))),r]| `2 by PSCOMP_1:def 6

.= r by EUCLID:52 ;

hence y in proj2 .: P by A13, A16, FUNCT_1:def 6; :: thesis: verum

end;
assume y in [.(- 1),1.] ; :: thesis: y in proj2 .: P

then y in { r where r is Real : ( - 1 <= r & r <= 1 ) } by RCOMP_1:def 1;

then consider r being Real such that

A13: y = r and

A14: ( - 1 <= r & r <= 1 ) ;

set q = |[(sqrt (1 - (r ^2))),r]|;

1 ^2 >= r ^2 by A14, SQUARE_1:49;

then A15: 1 - (r ^2) >= 0 by XREAL_1:48;

( |[(sqrt (1 - (r ^2))),r]| `2 = r & |[(sqrt (1 - (r ^2))),r]| `1 = sqrt (1 - (r ^2)) ) by EUCLID:52;

then |.|[(sqrt (1 - (r ^2))),r]|.| = sqrt (((sqrt (1 - (r ^2))) ^2) + (r ^2)) by JGRAPH_3:1

.= sqrt ((1 - (r ^2)) + (r ^2)) by A15, SQUARE_1:def 2

.= 1 by SQUARE_1:18 ;

then A16: ( dom proj2 = the carrier of (TOP-REAL 2) & |[(sqrt (1 - (r ^2))),r]| in P ) by A1, FUNCT_2:def 1;

proj2 . |[(sqrt (1 - (r ^2))),r]| = |[(sqrt (1 - (r ^2))),r]| `2 by PSCOMP_1:def 6

.= r by EUCLID:52 ;

hence y in proj2 .: P by A13, A16, FUNCT_1:def 6; :: thesis: verum

proof

hence
proj2 .: P = [.(- 1),1.]
by A12, XBOOLE_0:def 10; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 .: P or y in [.(- 1),1.] )

assume y in proj2 .: P ; :: thesis: y in [.(- 1),1.]

then consider x being object such that

A17: x in dom proj2 and

A18: x in P and

A19: y = proj2 . x by FUNCT_1:def 6;

reconsider q = x as Point of (TOP-REAL 2) by A17;

ex q2 being Point of (TOP-REAL 2) st

( q2 = x & |.q2.| = 1 ) by A1, A18;

then A20: ((q `1) ^2) + ((q `2) ^2) = 1 ^2 by JGRAPH_3:1;

0 <= (q `1) ^2 by XREAL_1:63;

then (1 - ((q `2) ^2)) + ((q `2) ^2) >= 0 + ((q `2) ^2) by A20, XREAL_1:7;

then A21: ( - 1 <= q `2 & q `2 <= 1 ) by SQUARE_1:51;

y = q `2 by A19, PSCOMP_1:def 6;

hence y in [.(- 1),1.] by A21, XXREAL_1:1; :: thesis: verum

end;
assume y in proj2 .: P ; :: thesis: y in [.(- 1),1.]

then consider x being object such that

A17: x in dom proj2 and

A18: x in P and

A19: y = proj2 . x by FUNCT_1:def 6;

reconsider q = x as Point of (TOP-REAL 2) by A17;

ex q2 being Point of (TOP-REAL 2) st

( q2 = x & |.q2.| = 1 ) by A1, A18;

then A20: ((q `1) ^2) + ((q `2) ^2) = 1 ^2 by JGRAPH_3:1;

0 <= (q `1) ^2 by XREAL_1:63;

then (1 - ((q `2) ^2)) + ((q `2) ^2) >= 0 + ((q `2) ^2) by A20, XREAL_1:7;

then A21: ( - 1 <= q `2 & q `2 <= 1 ) by SQUARE_1:51;

y = q `2 by A19, PSCOMP_1:def 6;

hence y in [.(- 1),1.] by A21, XXREAL_1:1; :: thesis: verum

Lm4: for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds

W-bound P = - 1

proof end;

theorem Th28: :: JGRAPH_5:28

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds

( W-bound P = - 1 & E-bound P = 1 & S-bound P = - 1 & N-bound P = 1 )

( W-bound P = - 1 & E-bound P = 1 & S-bound P = - 1 & N-bound P = 1 )

proof end;

theorem Th29: :: JGRAPH_5:29

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds

W-min P = |[(- 1),0]|

W-min P = |[(- 1),0]|

proof end;

theorem Th30: :: JGRAPH_5:30

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds

E-max P = |[1,0]|

E-max P = |[1,0]|

proof end;

theorem :: JGRAPH_5:31

for f being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds f . p = proj1 . p ) holds

f is continuous

f is continuous

proof end;

theorem Th32: :: JGRAPH_5:32

for f being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds f . p = proj2 . p ) holds

f is continuous

f is continuous

proof end;

theorem Th33: :: JGRAPH_5:33

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds

( Upper_Arc P c= P & Lower_Arc P c= P )

( Upper_Arc P c= P & Lower_Arc P c= P )

proof end;

theorem Th34: :: JGRAPH_5:34

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds

Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }

Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }

proof end;

theorem Th35: :: JGRAPH_5:35

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds

Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }

Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }

proof end;

theorem Th36: :: JGRAPH_5:36

for a, b, d, e being Real st a <= b & e > 0 holds

ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * a) + d),((e * b) + d))) st

( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds

f . r = (e * r) + d ) )

ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * a) + d),((e * b) + d))) st

( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds

f . r = (e * r) + d ) )

proof end;

theorem Th37: :: JGRAPH_5:37

for a, b, d, e being Real st a <= b & e < 0 holds

ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st

( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds

f . r = (e * r) + d ) )

ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st

( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds

f . r = (e * r) + d ) )

proof end;

theorem Th38: :: JGRAPH_5:38

ex f being Function of I[01],(Closed-Interval-TSpace ((- 1),1)) st

( f is being_homeomorphism & ( for r being Real st r in [.0,1.] holds

f . r = ((- 2) * r) + 1 ) & f . 0 = 1 & f . 1 = - 1 )

( f is being_homeomorphism & ( for r being Real st r in [.0,1.] holds

f . r = ((- 2) * r) + 1 ) & f . 0 = 1 & f . 1 = - 1 )

proof end;

theorem Th39: :: JGRAPH_5:39

ex f being Function of I[01],(Closed-Interval-TSpace ((- 1),1)) st

( f is being_homeomorphism & ( for r being Real st r in [.0,1.] holds

f . r = (2 * r) - 1 ) & f . 0 = - 1 & f . 1 = 1 )

( f is being_homeomorphism & ( for r being Real st r in [.0,1.] holds

f . r = (2 * r) - 1 ) & f . 0 = - 1 & f . 1 = 1 )

proof end;

Lm5: now :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds

( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )

( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )

reconsider B = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:17, XXREAL_1:1;

reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) )

set K0 = Lower_Arc P;

reconsider g2 = g | (Lower_Arc P) as Function of ((TOP-REAL 2) | (Lower_Arc P)),R^1 by PRE_TOPC:9;

A1: for p being Point of ((TOP-REAL 2) | (Lower_Arc P)) holds g2 . p = proj1 . p

then A3: Lower_Arc P c= P by Th33;

A4: dom g2 = the carrier of ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;

then A5: dom g2 = Lower_Arc P by PRE_TOPC:8;

rng g2 c= the carrier of (Closed-Interval-TSpace ((- 1),1))

dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;

then A11: dom g3 = Lower_Arc P by PRE_TOPC:def 5;

A12: for x, y being object st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds

x = y

g2 is continuous by A1, JGRAPH_2:29;

hence ( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) by A21, A27, A12, FUNCT_1:def 4, JGRAPH_1:45, XBOOLE_0:def 10; :: thesis: verum

end;
reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) )

set K0 = Lower_Arc P;

reconsider g2 = g | (Lower_Arc P) as Function of ((TOP-REAL 2) | (Lower_Arc P)),R^1 by PRE_TOPC:9;

A1: for p being Point of ((TOP-REAL 2) | (Lower_Arc P)) holds g2 . p = proj1 . p

proof

assume A2:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
; :: thesis: ( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )
let p be Point of ((TOP-REAL 2) | (Lower_Arc P)); :: thesis: g2 . p = proj1 . p

p in the carrier of ((TOP-REAL 2) | (Lower_Arc P)) ;

then p in Lower_Arc P by PRE_TOPC:8;

hence g2 . p = proj1 . p by FUNCT_1:49; :: thesis: verum

end;
p in the carrier of ((TOP-REAL 2) | (Lower_Arc P)) ;

then p in Lower_Arc P by PRE_TOPC:8;

hence g2 . p = proj1 . p by FUNCT_1:49; :: thesis: verum

then A3: Lower_Arc P c= P by Th33;

A4: dom g2 = the carrier of ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;

then A5: dom g2 = Lower_Arc P by PRE_TOPC:8;

rng g2 c= the carrier of (Closed-Interval-TSpace ((- 1),1))

proof

then reconsider g3 = g2 as Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) by A4, FUNCT_2:2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g2 or x in the carrier of (Closed-Interval-TSpace ((- 1),1)) )

assume x in rng g2 ; :: thesis: x in the carrier of (Closed-Interval-TSpace ((- 1),1))

then consider z being object such that

A6: z in dom g2 and

A7: x = g2 . z by FUNCT_1:def 3;

z in P by A5, A3, A6;

then consider p being Point of (TOP-REAL 2) such that

A8: p = z and

A9: |.p.| = 1 by A2;

1 ^2 = ((p `1) ^2) + ((p `2) ^2) by A9, JGRAPH_3:1;

then 1 - ((p `1) ^2) >= 0 by XREAL_1:63;

then - (1 - ((p `1) ^2)) <= 0 ;

then ((p `1) ^2) - 1 <= 0 ;

then A10: ( - 1 <= p `1 & p `1 <= 1 ) by SQUARE_1:43;

x = proj1 . p by A1, A6, A7, A8

.= p `1 by PSCOMP_1:def 5 ;

then x in [.(- 1),1.] by A10, XXREAL_1:1;

hence x in the carrier of (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18; :: thesis: verum

end;
assume x in rng g2 ; :: thesis: x in the carrier of (Closed-Interval-TSpace ((- 1),1))

then consider z being object such that

A6: z in dom g2 and

A7: x = g2 . z by FUNCT_1:def 3;

z in P by A5, A3, A6;

then consider p being Point of (TOP-REAL 2) such that

A8: p = z and

A9: |.p.| = 1 by A2;

1 ^2 = ((p `1) ^2) + ((p `2) ^2) by A9, JGRAPH_3:1;

then 1 - ((p `1) ^2) >= 0 by XREAL_1:63;

then - (1 - ((p `1) ^2)) <= 0 ;

then ((p `1) ^2) - 1 <= 0 ;

then A10: ( - 1 <= p `1 & p `1 <= 1 ) by SQUARE_1:43;

x = proj1 . p by A1, A6, A7, A8

.= p `1 by PSCOMP_1:def 5 ;

then x in [.(- 1),1.] by A10, XXREAL_1:1;

hence x in the carrier of (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18; :: thesis: verum

dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;

then A11: dom g3 = Lower_Arc P by PRE_TOPC:def 5;

A12: for x, y being object st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds

x = y

proof

A21:
[#] (Closed-Interval-TSpace ((- 1),1)) c= rng g3
let x, y be object ; :: thesis: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y implies x = y )

assume that

A13: x in dom g3 and

A14: y in dom g3 and

A15: g3 . x = g3 . y ; :: thesis: x = y

reconsider p2 = y as Point of (TOP-REAL 2) by A11, A14;

A16: g3 . y = proj1 . p2 by A1, A14

.= p2 `1 by PSCOMP_1:def 5 ;

reconsider p1 = x as Point of (TOP-REAL 2) by A11, A13;

A17: g3 . x = proj1 . p1 by A1, A13

.= p1 `1 by PSCOMP_1:def 5 ;

p2 in P by A3, A11, A14;

then ex p22 being Point of (TOP-REAL 2) st

( p2 = p22 & |.p22.| = 1 ) by A2;

then A18: 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;

p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A2, A11, A14, Th35;

then A19: ex p44 being Point of (TOP-REAL 2) st

( p2 = p44 & p44 in P & p44 `2 <= 0 ) ;

p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A2, A11, A13, Th35;

then A20: ex p33 being Point of (TOP-REAL 2) st

( p1 = p33 & p33 in P & p33 `2 <= 0 ) ;

p1 in P by A3, A11, A13;

then ex p11 being Point of (TOP-REAL 2) st

( p1 = p11 & |.p11.| = 1 ) by A2;

then 1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;

then (- (p1 `2)) ^2 = (p2 `2) ^2 by A15, A17, A16, A18;

then - (p1 `2) = sqrt ((- (p2 `2)) ^2) by A20, SQUARE_1:22;

then - (p1 `2) = - (p2 `2) by A19, SQUARE_1:22;

then p1 = |[(p2 `1),(p2 `2)]| by A15, A17, A16, EUCLID:53

.= p2 by EUCLID:53 ;

hence x = y ; :: thesis: verum

end;
assume that

A13: x in dom g3 and

A14: y in dom g3 and

A15: g3 . x = g3 . y ; :: thesis: x = y

reconsider p2 = y as Point of (TOP-REAL 2) by A11, A14;

A16: g3 . y = proj1 . p2 by A1, A14

.= p2 `1 by PSCOMP_1:def 5 ;

reconsider p1 = x as Point of (TOP-REAL 2) by A11, A13;

A17: g3 . x = proj1 . p1 by A1, A13

.= p1 `1 by PSCOMP_1:def 5 ;

p2 in P by A3, A11, A14;

then ex p22 being Point of (TOP-REAL 2) st

( p2 = p22 & |.p22.| = 1 ) by A2;

then A18: 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;

p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A2, A11, A14, Th35;

then A19: ex p44 being Point of (TOP-REAL 2) st

( p2 = p44 & p44 in P & p44 `2 <= 0 ) ;

p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A2, A11, A13, Th35;

then A20: ex p33 being Point of (TOP-REAL 2) st

( p1 = p33 & p33 in P & p33 `2 <= 0 ) ;

p1 in P by A3, A11, A13;

then ex p11 being Point of (TOP-REAL 2) st

( p1 = p11 & |.p11.| = 1 ) by A2;

then 1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;

then (- (p1 `2)) ^2 = (p2 `2) ^2 by A15, A17, A16, A18;

then - (p1 `2) = sqrt ((- (p2 `2)) ^2) by A20, SQUARE_1:22;

then - (p1 `2) = - (p2 `2) by A19, SQUARE_1:22;

then p1 = |[(p2 `1),(p2 `2)]| by A15, A17, A16, EUCLID:53

.= p2 by EUCLID:53 ;

hence x = y ; :: thesis: verum

proof

A27:
Closed-Interval-TSpace ((- 1),1) = R^1 | B
by TOPMETR:19;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (Closed-Interval-TSpace ((- 1),1)) or x in rng g3 )

assume x in [#] (Closed-Interval-TSpace ((- 1),1)) ; :: thesis: x in rng g3

then A22: x in [.(- 1),1.] by TOPMETR:18;

then reconsider r = x as Real ;

( - 1 <= r & r <= 1 ) by A22, XXREAL_1:1;

then 1 ^2 >= r ^2 by SQUARE_1:49;

then A23: 1 - (r ^2) >= 0 by XREAL_1:48;

set q = |[r,(- (sqrt (1 - (r ^2))))]|;

A24: |[r,(- (sqrt (1 - (r ^2))))]| `2 = - (sqrt (1 - (r ^2))) by EUCLID:52;

|.|[r,(- (sqrt (1 - (r ^2))))]|.| = sqrt (((|[r,(- (sqrt (1 - (r ^2))))]| `1) ^2) + ((|[r,(- (sqrt (1 - (r ^2))))]| `2) ^2)) by JGRAPH_3:1

.= sqrt ((r ^2) + ((|[r,(- (sqrt (1 - (r ^2))))]| `2) ^2)) by EUCLID:52

.= sqrt ((r ^2) + ((- (sqrt (1 - (r ^2)))) ^2)) by EUCLID:52

.= sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) ;

then |.|[r,(- (sqrt (1 - (r ^2))))]|.| = sqrt ((r ^2) + (1 - (r ^2))) by A23, SQUARE_1:def 2

.= 1 by SQUARE_1:18 ;

then A25: |[r,(- (sqrt (1 - (r ^2))))]| in P by A2;

0 <= sqrt (1 - (r ^2)) by A23, SQUARE_1:def 2;

then |[r,(- (sqrt (1 - (r ^2))))]| in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A25, A24;

then A26: |[r,(- (sqrt (1 - (r ^2))))]| in dom g3 by A2, A11, Th35;

then g3 . |[r,(- (sqrt (1 - (r ^2))))]| = proj1 . |[r,(- (sqrt (1 - (r ^2))))]| by A1

.= |[r,(- (sqrt (1 - (r ^2))))]| `1 by PSCOMP_1:def 5

.= r by EUCLID:52 ;

hence x in rng g3 by A26, FUNCT_1:def 3; :: thesis: verum

end;
assume x in [#] (Closed-Interval-TSpace ((- 1),1)) ; :: thesis: x in rng g3

then A22: x in [.(- 1),1.] by TOPMETR:18;

then reconsider r = x as Real ;

( - 1 <= r & r <= 1 ) by A22, XXREAL_1:1;

then 1 ^2 >= r ^2 by SQUARE_1:49;

then A23: 1 - (r ^2) >= 0 by XREAL_1:48;

set q = |[r,(- (sqrt (1 - (r ^2))))]|;

A24: |[r,(- (sqrt (1 - (r ^2))))]| `2 = - (sqrt (1 - (r ^2))) by EUCLID:52;

|.|[r,(- (sqrt (1 - (r ^2))))]|.| = sqrt (((|[r,(- (sqrt (1 - (r ^2))))]| `1) ^2) + ((|[r,(- (sqrt (1 - (r ^2))))]| `2) ^2)) by JGRAPH_3:1

.= sqrt ((r ^2) + ((|[r,(- (sqrt (1 - (r ^2))))]| `2) ^2)) by EUCLID:52

.= sqrt ((r ^2) + ((- (sqrt (1 - (r ^2)))) ^2)) by EUCLID:52

.= sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) ;

then |.|[r,(- (sqrt (1 - (r ^2))))]|.| = sqrt ((r ^2) + (1 - (r ^2))) by A23, SQUARE_1:def 2

.= 1 by SQUARE_1:18 ;

then A25: |[r,(- (sqrt (1 - (r ^2))))]| in P by A2;

0 <= sqrt (1 - (r ^2)) by A23, SQUARE_1:def 2;

then |[r,(- (sqrt (1 - (r ^2))))]| in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A25, A24;

then A26: |[r,(- (sqrt (1 - (r ^2))))]| in dom g3 by A2, A11, Th35;

then g3 . |[r,(- (sqrt (1 - (r ^2))))]| = proj1 . |[r,(- (sqrt (1 - (r ^2))))]| by A1

.= |[r,(- (sqrt (1 - (r ^2))))]| `1 by PSCOMP_1:def 5

.= r by EUCLID:52 ;

hence x in rng g3 by A26, FUNCT_1:def 3; :: thesis: verum

g2 is continuous by A1, JGRAPH_2:29;

hence ( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) by A21, A27, A12, FUNCT_1:def 4, JGRAPH_1:45, XBOOLE_0:def 10; :: thesis: verum

Lm6: now :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds

( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )

( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )

reconsider B = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:17, XXREAL_1:1;

reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) )

set K0 = Upper_Arc P;

reconsider g2 = g | (Upper_Arc P) as Function of ((TOP-REAL 2) | (Upper_Arc P)),R^1 by PRE_TOPC:9;

A1: for p being Point of ((TOP-REAL 2) | (Upper_Arc P)) holds g2 . p = proj1 . p

then A3: Upper_Arc P c= P by Th33;

A4: dom g2 = the carrier of ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;

then A5: dom g2 = Upper_Arc P by PRE_TOPC:8;

rng g2 c= the carrier of (Closed-Interval-TSpace ((- 1),1))

dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;

then A11: dom g3 = Upper_Arc P by PRE_TOPC:def 5;

A12: for x, y being object st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds

x = y

g2 is continuous by A1, JGRAPH_2:29;

hence ( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) by A21, A27, A12, FUNCT_1:def 4, JGRAPH_1:45, XBOOLE_0:def 10; :: thesis: verum

end;
reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) )

set K0 = Upper_Arc P;

reconsider g2 = g | (Upper_Arc P) as Function of ((TOP-REAL 2) | (Upper_Arc P)),R^1 by PRE_TOPC:9;

A1: for p being Point of ((TOP-REAL 2) | (Upper_Arc P)) holds g2 . p = proj1 . p

proof

assume A2:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
; :: thesis: ( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )
let p be Point of ((TOP-REAL 2) | (Upper_Arc P)); :: thesis: g2 . p = proj1 . p

p in the carrier of ((TOP-REAL 2) | (Upper_Arc P)) ;

then p in Upper_Arc P by PRE_TOPC:8;

hence g2 . p = proj1 . p by FUNCT_1:49; :: thesis: verum

end;
p in the carrier of ((TOP-REAL 2) | (Upper_Arc P)) ;

then p in Upper_Arc P by PRE_TOPC:8;

hence g2 . p = proj1 . p by FUNCT_1:49; :: thesis: verum

then A3: Upper_Arc P c= P by Th33;

A4: dom g2 = the carrier of ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;

then A5: dom g2 = Upper_Arc P by PRE_TOPC:8;

rng g2 c= the carrier of (Closed-Interval-TSpace ((- 1),1))

proof

then reconsider g3 = g2 as Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) by A4, FUNCT_2:2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g2 or x in the carrier of (Closed-Interval-TSpace ((- 1),1)) )

assume x in rng g2 ; :: thesis: x in the carrier of (Closed-Interval-TSpace ((- 1),1))

then consider z being object such that

A6: z in dom g2 and

A7: x = g2 . z by FUNCT_1:def 3;

z in P by A5, A3, A6;

then consider p being Point of (TOP-REAL 2) such that

A8: p = z and

A9: |.p.| = 1 by A2;

1 ^2 = ((p `1) ^2) + ((p `2) ^2) by A9, JGRAPH_3:1;

then 1 - ((p `1) ^2) >= 0 by XREAL_1:63;

then - (1 - ((p `1) ^2)) <= 0 ;

then ((p `1) ^2) - 1 <= 0 ;

then A10: ( - 1 <= p `1 & p `1 <= 1 ) by SQUARE_1:43;

x = proj1 . p by A1, A6, A7, A8

.= p `1 by PSCOMP_1:def 5 ;

then x in [.(- 1),1.] by A10, XXREAL_1:1;

hence x in the carrier of (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18; :: thesis: verum

end;
assume x in rng g2 ; :: thesis: x in the carrier of (Closed-Interval-TSpace ((- 1),1))

then consider z being object such that

A6: z in dom g2 and

A7: x = g2 . z by FUNCT_1:def 3;

z in P by A5, A3, A6;

then consider p being Point of (TOP-REAL 2) such that

A8: p = z and

A9: |.p.| = 1 by A2;

1 ^2 = ((p `1) ^2) + ((p `2) ^2) by A9, JGRAPH_3:1;

then 1 - ((p `1) ^2) >= 0 by XREAL_1:63;

then - (1 - ((p `1) ^2)) <= 0 ;

then ((p `1) ^2) - 1 <= 0 ;

then A10: ( - 1 <= p `1 & p `1 <= 1 ) by SQUARE_1:43;

x = proj1 . p by A1, A6, A7, A8

.= p `1 by PSCOMP_1:def 5 ;

then x in [.(- 1),1.] by A10, XXREAL_1:1;

hence x in the carrier of (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18; :: thesis: verum

dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;

then A11: dom g3 = Upper_Arc P by PRE_TOPC:def 5;

A12: for x, y being object st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds

x = y

proof

A21:
[#] (Closed-Interval-TSpace ((- 1),1)) c= rng g3
let x, y be object ; :: thesis: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y implies x = y )

assume that

A13: x in dom g3 and

A14: y in dom g3 and

A15: g3 . x = g3 . y ; :: thesis: x = y

reconsider p2 = y as Point of (TOP-REAL 2) by A11, A14;

A16: g3 . y = proj1 . p2 by A1, A14

.= p2 `1 by PSCOMP_1:def 5 ;

reconsider p1 = x as Point of (TOP-REAL 2) by A11, A13;

A17: g3 . x = proj1 . p1 by A1, A13

.= p1 `1 by PSCOMP_1:def 5 ;

p2 in P by A3, A11, A14;

then ex p22 being Point of (TOP-REAL 2) st

( p2 = p22 & |.p22.| = 1 ) by A2;

then A18: 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;

p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A2, A11, A14, Th34;

then A19: ex p44 being Point of (TOP-REAL 2) st

( p2 = p44 & p44 in P & p44 `2 >= 0 ) ;

p1 in P by A3, A11, A13;

then ex p11 being Point of (TOP-REAL 2) st

( p1 = p11 & |.p11.| = 1 ) by A2;

then A20: 1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;

p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A2, A11, A13, Th34;

then ex p33 being Point of (TOP-REAL 2) st

( p1 = p33 & p33 in P & p33 `2 >= 0 ) ;

then p1 `2 = sqrt ((p2 `2) ^2) by A15, A17, A16, A18, A20, SQUARE_1:22;

then p1 `2 = p2 `2 by A19, SQUARE_1:22;

then p1 = |[(p2 `1),(p2 `2)]| by A15, A17, A16, EUCLID:53

.= p2 by EUCLID:53 ;

hence x = y ; :: thesis: verum

end;
assume that

A13: x in dom g3 and

A14: y in dom g3 and

A15: g3 . x = g3 . y ; :: thesis: x = y

reconsider p2 = y as Point of (TOP-REAL 2) by A11, A14;

A16: g3 . y = proj1 . p2 by A1, A14

.= p2 `1 by PSCOMP_1:def 5 ;

reconsider p1 = x as Point of (TOP-REAL 2) by A11, A13;

A17: g3 . x = proj1 . p1 by A1, A13

.= p1 `1 by PSCOMP_1:def 5 ;

p2 in P by A3, A11, A14;

then ex p22 being Point of (TOP-REAL 2) st

( p2 = p22 & |.p22.| = 1 ) by A2;

then A18: 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;

p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A2, A11, A14, Th34;

then A19: ex p44 being Point of (TOP-REAL 2) st

( p2 = p44 & p44 in P & p44 `2 >= 0 ) ;

p1 in P by A3, A11, A13;

then ex p11 being Point of (TOP-REAL 2) st

( p1 = p11 & |.p11.| = 1 ) by A2;

then A20: 1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;

p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A2, A11, A13, Th34;

then ex p33 being Point of (TOP-REAL 2) st

( p1 = p33 & p33 in P & p33 `2 >= 0 ) ;

then p1 `2 = sqrt ((p2 `2) ^2) by A15, A17, A16, A18, A20, SQUARE_1:22;

then p1 `2 = p2 `2 by A19, SQUARE_1:22;

then p1 = |[(p2 `1),(p2 `2)]| by A15, A17, A16, EUCLID:53

.= p2 by EUCLID:53 ;

hence x = y ; :: thesis: verum

proof

A27:
Closed-Interval-TSpace ((- 1),1) = R^1 | B
by TOPMETR:19;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (Closed-Interval-TSpace ((- 1),1)) or x in rng g3 )

assume x in [#] (Closed-Interval-TSpace ((- 1),1)) ; :: thesis: x in rng g3

then A22: x in [.(- 1),1.] by TOPMETR:18;

then reconsider r = x as Real ;

( - 1 <= r & r <= 1 ) by A22, XXREAL_1:1;

then 1 ^2 >= r ^2 by SQUARE_1:49;

then A23: 1 - (r ^2) >= 0 by XREAL_1:48;

set q = |[r,(sqrt (1 - (r ^2)))]|;

A24: |[r,(sqrt (1 - (r ^2)))]| `2 = sqrt (1 - (r ^2)) by EUCLID:52;

|.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt (((|[r,(sqrt (1 - (r ^2)))]| `1) ^2) + ((|[r,(sqrt (1 - (r ^2)))]| `2) ^2)) by JGRAPH_3:1

.= sqrt ((r ^2) + ((|[r,(sqrt (1 - (r ^2)))]| `2) ^2)) by EUCLID:52

.= sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) by EUCLID:52 ;

then |.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt ((r ^2) + (1 - (r ^2))) by A23, SQUARE_1:def 2

.= 1 by SQUARE_1:18 ;

then A25: |[r,(sqrt (1 - (r ^2)))]| in P by A2;

0 <= sqrt (1 - (r ^2)) by A23, SQUARE_1:def 2;

then |[r,(sqrt (1 - (r ^2)))]| in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A25, A24;

then A26: |[r,(sqrt (1 - (r ^2)))]| in dom g3 by A2, A11, Th34;

then g3 . |[r,(sqrt (1 - (r ^2)))]| = proj1 . |[r,(sqrt (1 - (r ^2)))]| by A1

.= |[r,(sqrt (1 - (r ^2)))]| `1 by PSCOMP_1:def 5

.= r by EUCLID:52 ;

hence x in rng g3 by A26, FUNCT_1:def 3; :: thesis: verum

end;
assume x in [#] (Closed-Interval-TSpace ((- 1),1)) ; :: thesis: x in rng g3

then A22: x in [.(- 1),1.] by TOPMETR:18;

then reconsider r = x as Real ;

( - 1 <= r & r <= 1 ) by A22, XXREAL_1:1;

then 1 ^2 >= r ^2 by SQUARE_1:49;

then A23: 1 - (r ^2) >= 0 by XREAL_1:48;

set q = |[r,(sqrt (1 - (r ^2)))]|;

A24: |[r,(sqrt (1 - (r ^2)))]| `2 = sqrt (1 - (r ^2)) by EUCLID:52;

|.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt (((|[r,(sqrt (1 - (r ^2)))]| `1) ^2) + ((|[r,(sqrt (1 - (r ^2)))]| `2) ^2)) by JGRAPH_3:1

.= sqrt ((r ^2) + ((|[r,(sqrt (1 - (r ^2)))]| `2) ^2)) by EUCLID:52

.= sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) by EUCLID:52 ;

then |.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt ((r ^2) + (1 - (r ^2))) by A23, SQUARE_1:def 2

.= 1 by SQUARE_1:18 ;

then A25: |[r,(sqrt (1 - (r ^2)))]| in P by A2;

0 <= sqrt (1 - (r ^2)) by A23, SQUARE_1:def 2;

then |[r,(sqrt (1 - (r ^2)))]| in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A25, A24;

then A26: |[r,(sqrt (1 - (r ^2)))]| in dom g3 by A2, A11, Th34;

then g3 . |[r,(sqrt (1 - (r ^2)))]| = proj1 . |[r,(sqrt (1 - (r ^2)))]| by A1

.= |[r,(sqrt (1 - (r ^2)))]| `1 by PSCOMP_1:def 5

.= r by EUCLID:52 ;

hence x in rng g3 by A26, FUNCT_1:def 3; :: thesis: verum

g2 is continuous by A1, JGRAPH_2:29;

hence ( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) by A21, A27, A12, FUNCT_1:def 4, JGRAPH_1:45, XBOOLE_0:def 10; :: thesis: verum

theorem Th40: :: JGRAPH_5:40

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds

ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Lower_Arc P)) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds

f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )

ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Lower_Arc P)) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds

f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )

proof end;

theorem Th41: :: JGRAPH_5:41

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds

ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Upper_Arc P)) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds

f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )

ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Upper_Arc P)) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds

f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )

proof end;

theorem Th42: :: JGRAPH_5:42

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds

ex f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)) st

( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)

for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds

( r1 < r2 iff q1 `1 > q2 `1 ) ) & f . 0 = E-max P & f . 1 = W-min P )

ex f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)) st

( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)

for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds

( r1 < r2 iff q1 `1 > q2 `1 ) ) & f . 0 = E-max P & f . 1 = W-min P )

proof end;

theorem Th43: :: JGRAPH_5:43

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds

ex f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)) st

( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)

for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds

( r1 < r2 iff q1 `1 < q2 `1 ) ) & f . 0 = W-min P & f . 1 = E-max P )

ex f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)) st

( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)

for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds

( r1 < r2 iff q1 `1 < q2 `1 ) ) & f . 0 = W-min P & f . 1 = E-max P )

proof end;

theorem Th44: :: JGRAPH_5:44

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p2 in Upper_Arc P & LE p1,p2,P holds

p1 in Upper_Arc P

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p2 in Upper_Arc P & LE p1,p2,P holds

p1 in Upper_Arc P

proof end;

theorem Th45: :: JGRAPH_5:45

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 holds

( p1 `1 > p2 `1 & p1 `2 < p2 `2 )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 holds

( p1 `1 > p2 `1 & p1 `2 < p2 `2 )

proof end;

theorem Th46: :: JGRAPH_5:46

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 holds

( p1 `1 < p2 `1 & p1 `2 < p2 `2 )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 holds

( p1 `1 < p2 `1 & p1 `2 < p2 `2 )

proof end;

theorem Th47: :: JGRAPH_5:47

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p2 `2 >= 0 holds

p1 `1 < p2 `1

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p2 `2 >= 0 holds

p1 `1 < p2 `1

proof end;

theorem Th48: :: JGRAPH_5:48

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `2 <= 0 & p1 <> W-min P holds

p1 `1 > p2 `1

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `2 <= 0 & p1 <> W-min P holds

p1 `1 > p2 `1

proof end;

theorem Th49: :: JGRAPH_5:49

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & ( p2 `2 >= 0 or p2 `1 >= 0 ) & LE p1,p2,P & not p1 `2 >= 0 holds

p1 `1 >= 0

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & ( p2 `2 >= 0 or p2 `1 >= 0 ) & LE p1,p2,P & not p1 `2 >= 0 holds

p1 `1 >= 0

proof end;

theorem Th50: :: JGRAPH_5:50

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `1 >= 0 & p2 `1 >= 0 holds

p1 `2 > p2 `2

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & p1 <> p2 & p1 `1 >= 0 & p2 `1 >= 0 holds

p1 `2 > p2 `2

proof end;

theorem Th51: :: JGRAPH_5:51

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 < 0 & p2 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 <= p2 `2 ) holds

LE p1,p2,P

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 < 0 & p2 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 <= p2 `2 ) holds

LE p1,p2,P

proof end;

theorem :: JGRAPH_5:52

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 > 0 & p2 `1 > 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) holds

LE p1,p2,P

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 > 0 & p2 `1 > 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) holds

LE p1,p2,P

proof end;

theorem Th53: :: JGRAPH_5:53

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 < 0 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 & ( p1 `1 <= p2 `1 or p1 `2 <= p2 `2 ) holds

LE p1,p2,P

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 < 0 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 & ( p1 `1 <= p2 `1 or p1 `2 <= p2 `2 ) holds

LE p1,p2,P

proof end;

theorem Th54: :: JGRAPH_5:54

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `2 >= 0 & p2 `2 >= 0 & p1 `1 <= p2 `1 holds

LE p1,p2,P

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `2 >= 0 & p2 `2 >= 0 & p1 `1 <= p2 `1 holds

LE p1,p2,P

proof end;

theorem Th55: :: JGRAPH_5:55

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 >= 0 & p2 `1 >= 0 & p1 `2 >= p2 `2 holds

LE p1,p2,P

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `1 >= 0 & p2 `1 >= 0 & p1 `2 >= p2 `2 holds

LE p1,p2,P

proof end;

theorem Th56: :: JGRAPH_5:56

for p1, p2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `2 <= 0 & p2 `2 <= 0 & p2 <> W-min P & p1 `1 >= p2 `1 holds

LE p1,p2,P

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p1 `2 <= 0 & p2 `2 <= 0 & p2 <> W-min P & p1 `1 >= p2 `1 holds

LE p1,p2,P

proof end;

theorem Th57: :: JGRAPH_5:57

for cn being Real

for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 <= 0 holds

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds

p `2 <= 0

for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 <= 0 holds

for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds

p `2 <= 0

proof end;

theorem Th58: :: JGRAPH_5:58

for cn being Real

for p1, p2, q1, q2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st - 1 < cn & cn < 1 & P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & q1 = (cn -FanMorphS) . p1 & q2 = (cn -FanMorphS) . p2 holds

LE q1,q2,P

for p1, p2, q1, q2 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st - 1 < cn & cn < 1 & P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & q1 = (cn -FanMorphS) . p1 & q2 = (cn -FanMorphS) . p2 holds

LE q1,q2,P

proof end;

theorem Th59: :: JGRAPH_5:59

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 `1 < 0 & p1 `2 >= 0 & p2 `1 < 0 & p2 `2 >= 0 & p3 `1 < 0 & p3 `2 >= 0 & p4 `1 < 0 & p4 `2 >= 0 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 `1 < 0 & p1 `2 >= 0 & p2 `1 < 0 & p2 `2 >= 0 & p3 `1 < 0 & p3 `2 >= 0 & p4 `1 < 0 & p4 `2 >= 0 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

proof end;

theorem Th60: :: JGRAPH_5:60

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 `2 >= 0 & p2 `2 >= 0 & p3 `2 >= 0 & p4 `2 > 0 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 >= 0 & q2 `1 < 0 & q2 `2 >= 0 & q3 `1 < 0 & q3 `2 >= 0 & q4 `1 < 0 & q4 `2 >= 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 `2 >= 0 & p2 `2 >= 0 & p3 `2 >= 0 & p4 `2 > 0 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 >= 0 & q2 `1 < 0 & q2 `2 >= 0 & q3 `1 < 0 & q3 `2 >= 0 & q4 `1 < 0 & q4 `2 >= 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

proof end;

theorem Th61: :: JGRAPH_5:61

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 `2 >= 0 & p2 `2 >= 0 & p3 `2 >= 0 & p4 `2 > 0 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 `2 >= 0 & p2 `2 >= 0 & p3 `2 >= 0 & p4 `2 > 0 holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

proof end;

theorem Th62: :: JGRAPH_5:62

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

proof end;

theorem Th63: :: JGRAPH_5:63

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

proof end;

theorem :: JGRAPH_5:64

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p4 = W-min P & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p4 = W-min P & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

proof end;

theorem Th65: :: JGRAPH_5:65

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )

proof end;

theorem Th66: :: JGRAPH_5:66

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 <> p2 & p2 <> p3 & p3 <> p4 & p1 `1 < 0 & p2 `1 < 0 & p3 `1 < 0 & p4 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 & p3 `2 < 0 holds

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

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0]| = f . p1 & |[0,1]| = f . p2 & |[1,0]| = f . p3 & |[0,(- 1)]| = f . p4 )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 <> p2 & p2 <> p3 & p3 <> p4 & p1 `1 < 0 & p2 `1 < 0 & p3 `1 < 0 & p4 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 & p3 `2 < 0 holds

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

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0]| = f . p1 & |[0,1]| = f . p2 & |[1,0]| = f . p3 & |[0,(- 1)]| = f . p4 )

proof end;

theorem Th67: :: JGRAPH_5:67

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 <> p2 & p2 <> p3 & p3 <> p4 holds

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

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0]| = f . p1 & |[0,1]| = f . p2 & |[1,0]| = f . p3 & |[0,(- 1)]| = f . p4 )

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 <> p2 & p2 <> p3 & p3 <> p4 holds

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

( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0]| = f . p1 & |[0,1]| = f . p2 & |[1,0]| = f . p3 & |[0,(- 1)]| = f . p4 )

proof end;

Lm7: |[(- 1),0]| `1 = - 1

by EUCLID:52;

Lm8: |[(- 1),0]| `2 = 0

by EUCLID:52;

Lm9: ( |[1,0]| `1 = 1 & |[1,0]| `2 = 0 )

by EUCLID:52;

Lm10: |[0,(- 1)]| `1 = 0

by EUCLID:52;

Lm11: |[0,(- 1)]| `2 = - 1

by EUCLID:52;

Lm12: |[0,1]| `1 = 0

by EUCLID:52;

Lm13: |[0,1]| `2 = 1

by EUCLID:52;

Lm14: now :: thesis: ( |.|[(- 1),0]|.| = 1 & |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[(- 1),0]|.| =
sqrt (((- 1) ^2) + (0 ^2))
by Lm7, Lm8, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by Lm9, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[0,(- 1)]|.| = sqrt ((0 ^2) + ((- 1) ^2)) by Lm10, Lm11, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: |.|[0,1]|.| = 1

thus |.|[0,1]|.| = sqrt ((0 ^2) + (1 ^2)) by Lm12, Lm13, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: verum

end;
.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by Lm9, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[0,(- 1)]|.| = sqrt ((0 ^2) + ((- 1) ^2)) by Lm10, Lm11, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: |.|[0,1]|.| = 1

thus |.|[0,1]|.| = sqrt ((0 ^2) + (1 ^2)) by Lm12, Lm13, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: verum

Lm15: 0 in [.0,1.]

by XXREAL_1:1;

Lm16: 1 in [.0,1.]

by XXREAL_1:1;

theorem :: JGRAPH_5:68

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

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

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

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

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;

theorem :: JGRAPH_5:69

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

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

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

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

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;

theorem :: JGRAPH_5:70

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

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

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

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

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;

theorem :: JGRAPH_5:71

for p1, p2, p3, p4 being Point of (TOP-REAL 2)

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

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

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

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds

for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

proof end;