:: by Yatsuka Nakamura

::

:: Received August 20, 2001

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

Lm1: for x being Real holds (x ^2) + 1 > 0

proof end;

Lm2: dom proj1 = the carrier of (TOP-REAL 2)

by FUNCT_2:def 1;

Lm3: dom proj2 = the carrier of (TOP-REAL 2)

by FUNCT_2:def 1;

theorem :: JGRAPH_3:1

theorem Th3: :: JGRAPH_3:3

for X, Y being non empty TopSpace

for p0 being Point of X

for D being non empty Subset of X

for E being non empty Subset of Y

for f being Function of X,Y st D ` = {p0} & E ` = {(f . p0)} & X is T_2 & Y is T_2 & ( for p being Point of (X | D) holds f . p <> f . p0 ) & f | D is continuous Function of (X | D),(Y | E) & ( for V being Subset of Y st f . p0 in V & V is open holds

ex W being Subset of X st

( p0 in W & W is open & f .: W c= V ) ) holds

f is continuous

for p0 being Point of X

for D being non empty Subset of X

for E being non empty Subset of Y

for f being Function of X,Y st D ` = {p0} & E ` = {(f . p0)} & X is T_2 & Y is T_2 & ( for p being Point of (X | D) holds f . p <> f . p0 ) & f | D is continuous Function of (X | D),(Y | E) & ( for V being Subset of Y st f . p0 in V & V is open holds

ex W being Subset of X st

( p0 in W & W is open & f .: W c= V ) ) holds

f is continuous

proof end;

definition

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

for p being Point of (TOP-REAL 2) holds

( ( p = 0. (TOP-REAL 2) implies b_{1} . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies b_{1} . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or b_{1} . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )

for b_{1}, b_{2} being Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds

( ( p = 0. (TOP-REAL 2) implies b_{1} . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies b_{1} . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or b_{1} . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) ) ) & ( for p being Point of (TOP-REAL 2) holds

( ( p = 0. (TOP-REAL 2) implies b_{2} . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies b_{2} . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or b_{2} . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) ) ) holds

b_{1} = b_{2}
end;

func Sq_Circ -> Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) means :Def1: :: JGRAPH_3:def 1

for p being Point of (TOP-REAL 2) holds

( ( p = 0. (TOP-REAL 2) implies it . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies it . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or it . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) );

existence for p being Point of (TOP-REAL 2) holds

( ( p = 0. (TOP-REAL 2) implies it . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies it . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or it . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) );

ex b

for p being Point of (TOP-REAL 2) holds

( ( p = 0. (TOP-REAL 2) implies b

proof end;

uniqueness for b

( ( p = 0. (TOP-REAL 2) implies b

( ( p = 0. (TOP-REAL 2) implies b

b

proof end;

:: deftheorem Def1 defines Sq_Circ JGRAPH_3:def 1 :

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

( b_{1} = Sq_Circ iff for p being Point of (TOP-REAL 2) holds

( ( p = 0. (TOP-REAL 2) implies b_{1} . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies b_{1} . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or b_{1} . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) ) );

for b

( b

( ( p = 0. (TOP-REAL 2) implies b

theorem Th4: :: JGRAPH_3:4

for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) implies Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) )

( ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) implies Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) )

proof end;

theorem Th5: :: JGRAPH_3:5

for X being non empty TopSpace

for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X ex r being Real st

( f1 . q = r & r >= 0 ) ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous )

for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X ex r being Real st

( f1 . q = r & r >= 0 ) ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = sqrt r1 ) & g is continuous )

proof end;

theorem Th6: :: JGRAPH_3:6

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = (r1 / r2) ^2 ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = (r1 / r2) ^2 ) & g is continuous )

proof end;

theorem Th7: :: JGRAPH_3:7

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = 1 + ((r1 / r2) ^2) ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = 1 + ((r1 / r2) ^2) ) & g is continuous )

proof end;

theorem Th8: :: JGRAPH_3:8

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = sqrt (1 + ((r1 / r2) ^2)) ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = sqrt (1 + ((r1 / r2) ^2)) ) & g is continuous )

proof end;

theorem Th9: :: JGRAPH_3:9

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

proof end;

theorem Th10: :: JGRAPH_3:10

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r2 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r2 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

proof end;

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

for q being Point of ((TOP-REAL 2) | K1) holds (proj2 | K1) . q = proj2 . q

proof end;

Lm5: for K1 being non empty Subset of (TOP-REAL 2) holds proj2 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1

proof end;

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

for q being Point of ((TOP-REAL 2) | K1) holds (proj1 | K1) . q = proj1 . q

proof end;

Lm7: for K1 being non empty Subset of (TOP-REAL 2) holds proj1 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1

proof end;

theorem Th11: :: JGRAPH_3:11

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

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

proof end;

theorem Th12: :: JGRAPH_3:12

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

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

proof end;

theorem Th13: :: JGRAPH_3:13

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

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

proof end;

theorem Th14: :: JGRAPH_3:14

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

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

proof end;

Lm8: 0.REAL 2 = 0. (TOP-REAL 2)

by EUCLID:66;

Lm9: ( ( (1.REAL 2) `2 <= (1.REAL 2) `1 & - ((1.REAL 2) `1) <= (1.REAL 2) `2 ) or ( (1.REAL 2) `2 >= (1.REAL 2) `1 & (1.REAL 2) `2 <= - ((1.REAL 2) `1) ) )

by JGRAPH_2:5;

Lm10: 1.REAL 2 <> 0. (TOP-REAL 2)

by Lm8, REVROT_1:19;

Lm11: for K1 being non empty Subset of (TOP-REAL 2) holds dom (proj2 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)

proof end;

Lm12: for K1 being non empty Subset of (TOP-REAL 2) holds dom (proj1 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)

proof end;

Lm13: NonZero (TOP-REAL 2) <> {}

by JGRAPH_2:9;

theorem Th15: :: JGRAPH_3:15

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

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

f is continuous

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

f is continuous

proof end;

Lm14: ( ( (1.REAL 2) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2) ) )

by JGRAPH_2:5;

Lm15: 1.REAL 2 <> 0. (TOP-REAL 2)

by Lm8, REVROT_1:19;

theorem Th16: :: JGRAPH_3:16

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

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

f is continuous

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

f is continuous

proof end;

theorem Th17: :: JGRAPH_3:17

for B0 being Subset of (TOP-REAL 2)

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

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

( f is continuous & K0 is closed )

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

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

( f is continuous & K0 is closed )

proof end;

theorem Th18: :: JGRAPH_3:18

for B0 being Subset of (TOP-REAL 2)

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

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

( f is continuous & K0 is closed )

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

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

( f is continuous & K0 is closed )

proof end;

theorem Th19: :: JGRAPH_3:19

for D being non empty Subset of (TOP-REAL 2) st D ` = {(0. (TOP-REAL 2))} holds

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

( h = Sq_Circ | D & h is continuous )

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

( h = Sq_Circ | D & h is continuous )

proof end;

theorem Th20: :: JGRAPH_3:20

for D being non empty Subset of (TOP-REAL 2) st D = NonZero (TOP-REAL 2) holds

D ` = {(0. (TOP-REAL 2))}

D ` = {(0. (TOP-REAL 2))}

proof end;

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

by EUCLID:def 8;

theorem Th23: :: JGRAPH_3:23

for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = 1 } holds

Sq_Circ .: Kb = Cb

Sq_Circ .: Kb = Cb

proof end;

theorem Th24: :: JGRAPH_3:24

for P, Kb being Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | P) st Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } & f is being_homeomorphism holds

P is being_simple_closed_curve

for f being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | P) st Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } & f is being_homeomorphism holds

P is being_simple_closed_curve

proof end;

theorem Th25: :: JGRAPH_3:25

for Kb being Subset of (TOP-REAL 2) st Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } holds

( Kb is being_simple_closed_curve & Kb is compact )

( Kb is being_simple_closed_curve & Kb is compact )

proof end;

theorem :: JGRAPH_3:26

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

Cb is being_simple_closed_curve

Cb is being_simple_closed_curve

proof end;

theorem :: JGRAPH_3:27

for K0, C0 being Subset of (TOP-REAL 2) st K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & C0 = { p1 where p1 is Point of (TOP-REAL 2) : |.p1.| <= 1 } holds

Sq_Circ " C0 c= K0

Sq_Circ " C0 c= K0

proof end;

theorem Th28: :: JGRAPH_3:28

for p being Point of (TOP-REAL 2) holds

( ( p = 0. (TOP-REAL 2) implies (Sq_Circ ") . p = 0. (TOP-REAL 2) ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )

( ( p = 0. (TOP-REAL 2) implies (Sq_Circ ") . p = 0. (TOP-REAL 2) ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )

proof end;

theorem Th30: :: JGRAPH_3:30

for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) implies (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) )

( ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) implies (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) )

proof end;

theorem Th31: :: JGRAPH_3:31

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

proof end;

theorem Th32: :: JGRAPH_3:32

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r2 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r2 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )

proof end;

theorem Th33: :: JGRAPH_3:33

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

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) * (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

proof end;

theorem Th34: :: JGRAPH_3:34

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

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `2) * (sqrt (1 + (((p `2) / (p `1)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

proof end;

theorem Th35: :: JGRAPH_3:35

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

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

proof end;

theorem Th36: :: JGRAPH_3:36

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

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = (p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2))) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

proof end;

Lm17: for K1 being non empty Subset of (TOP-REAL 2) holds proj2 * ((Sq_Circ ") | K1) is Function of ((TOP-REAL 2) | K1),R^1

proof end;

Lm18: for K1 being non empty Subset of (TOP-REAL 2) holds proj1 * ((Sq_Circ ") | K1) is Function of ((TOP-REAL 2) | K1),R^1

proof end;

theorem Th37: :: JGRAPH_3:37

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

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

f is continuous

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

f is continuous

proof end;

theorem Th38: :: JGRAPH_3:38

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

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

f is continuous

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

f is continuous

proof end;

theorem Th39: :: JGRAPH_3:39

for B0 being Subset of (TOP-REAL 2)

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

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

( f is continuous & K0 is closed )

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

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

( f is continuous & K0 is closed )

proof end;

theorem Th40: :: JGRAPH_3:40

for B0 being Subset of (TOP-REAL 2)

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

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

( f is continuous & K0 is closed )

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

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

( f is continuous & K0 is closed )

proof end;

theorem Th41: :: JGRAPH_3:41

for D being non empty Subset of (TOP-REAL 2) st D ` = {(0. (TOP-REAL 2))} holds

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

( h = (Sq_Circ ") | D & h is continuous )

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

( h = (Sq_Circ ") | D & h is continuous )

proof end;

theorem Th43: :: JGRAPH_3:43

( Sq_Circ is Function of (TOP-REAL 2),(TOP-REAL 2) & rng Sq_Circ = the carrier of (TOP-REAL 2) & ( for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds

f is being_homeomorphism ) )

f is being_homeomorphism ) )

proof end;

Lm19: now :: thesis: for pz2, pz1 being Real st (((pz2 ^2) + (pz1 ^2)) - 1) * (pz2 ^2) <= pz1 ^2 holds

((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0

((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0

let pz2, pz1 be Real; :: thesis: ( (((pz2 ^2) + (pz1 ^2)) - 1) * (pz2 ^2) <= pz1 ^2 implies ((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0 )

assume (((pz2 ^2) + (pz1 ^2)) - 1) * (pz2 ^2) <= pz1 ^2 ; :: thesis: ((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0

then (((pz2 ^2) * (pz2 ^2)) + ((pz2 ^2) * ((pz1 ^2) - 1))) - (pz1 ^2) <= (pz1 ^2) - (pz1 ^2) by XREAL_1:9;

hence ((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0 ; :: thesis: verum

end;
assume (((pz2 ^2) + (pz1 ^2)) - 1) * (pz2 ^2) <= pz1 ^2 ; :: thesis: ((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0

then (((pz2 ^2) * (pz2 ^2)) + ((pz2 ^2) * ((pz1 ^2) - 1))) - (pz1 ^2) <= (pz1 ^2) - (pz1 ^2) by XREAL_1:9;

hence ((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0 ; :: thesis: verum

Lm20: now :: thesis: for px1 being Real holds

( not (px1 ^2) - 1 = 0 or px1 = 1 or px1 = - 1 )

( not (px1 ^2) - 1 = 0 or px1 = 1 or px1 = - 1 )

let px1 be Real; :: thesis: ( not (px1 ^2) - 1 = 0 or px1 = 1 or px1 = - 1 )

assume (px1 ^2) - 1 = 0 ; :: thesis: ( px1 = 1 or px1 = - 1 )

then (px1 - 1) * (px1 + 1) = 0 ;

then ( px1 - 1 = 0 or px1 + 1 = 0 ) by XCMPLX_1:6;

hence ( px1 = 1 or px1 = - 1 ) ; :: thesis: verum

end;
assume (px1 ^2) - 1 = 0 ; :: thesis: ( px1 = 1 or px1 = - 1 )

then (px1 - 1) * (px1 + 1) = 0 ;

then ( px1 - 1 = 0 or px1 + 1 = 0 ) by XCMPLX_1:6;

hence ( px1 = 1 or px1 = - 1 ) ; :: thesis: verum

theorem :: JGRAPH_3:44

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;