:: JGRAPH_2 semantic presentation

Lm1: TOP-REAL 2 = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;

theorem :: JGRAPH_2:1

canceled;

theorem Th2: :: JGRAPH_2:2

for a being real number st 1 <= a holds
a <= a ^2 by REAL_2:146;

theorem :: JGRAPH_2:3

for a being real number st - 1 >= a holds
- a <= a ^2

proof end;

theorem Th4: :: JGRAPH_2:4

for a being real number st - 1 > a holds
- a < a ^2

proof end;

theorem Th5: :: JGRAPH_2:5

for a, b being real number st b ^2 <= a ^2 & a >= 0 holds
( - a <= b & b <= a )

proof end;

theorem Th6: :: JGRAPH_2:6

for a, b being real number st b ^2 < a ^2 & a >= 0 holds
( - a < b & b < a )

proof end;

theorem :: JGRAPH_2:7

for a, b being real number st - a <= b & b <= a holds
b ^2 <= a ^2

proof end;

theorem Th8: :: JGRAPH_2:8

for a, b being real number st - a < b & b < a holds
b ^2 < a ^2

proof end;

theorem Th9: :: JGRAPH_2:9

for T1, S, T2, T being non empty TopSpace
for f being Function of T1,S
for g being Function of T2,S
for F1, F2 being Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & F1 is closed & F2 is closed & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds
f . p = g . p ) holds
ex h being Function of T,S st
( h = f +* g & h is continuous )

proof end;

theorem Th10: :: JGRAPH_2:10

for n being Nat
for q2 being Point of (Euclid n)
for q being Point of (TOP-REAL n)
for r being real number st q = q2 holds
Ball q2,r = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }

proof end;

theorem Th11: :: JGRAPH_2:11

( (0.REAL 2) `1 = 0 & (0.REAL 2) `2 = 0 ) by EUCLID:56, EUCLID:58;

theorem Th12: :: JGRAPH_2:12

1.REAL 2 = <*1,1*>

proof end;

theorem Th13: :: JGRAPH_2:13

( (1.REAL 2) `1 = 1 & (1.REAL 2) `2 = 1 )

proof end;

theorem Th14: :: JGRAPH_2:14

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

proof end;

theorem Th15: :: JGRAPH_2:15

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

proof end;

theorem :: JGRAPH_2:16

canceled;

theorem :: JGRAPH_2:17

canceled;

theorem Th18: :: JGRAPH_2:18

for p being Point of (TOP-REAL 2) holds p = |[(proj1 . p),(proj2 . p)]|

proof end;

theorem Th19: :: JGRAPH_2:19

for B being Subset of (TOP-REAL 2) st B = {(0.REAL 2)} holds
( B ` <> {} & the carrier of (TOP-REAL 2) \ B <> {} )

proof end;

theorem Th20: :: JGRAPH_2:20

for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff for p being Point of X
for V being Subset of Y st f . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & f .: W c= V ) )

proof end;

theorem Th21: :: JGRAPH_2:21

for p being Point of (TOP-REAL 2)
for G being Subset of (TOP-REAL 2) st G is open & p in G holds
ex r being real number st
( r > 0 & { q where q is Point of (TOP-REAL 2) : ( (p `1 ) - r < q `1 & q `1 < (p `1 ) + r & (p `2 ) - r < q `2 & q `2 < (p `2 ) + r ) } c= G )

proof end;

theorem Th22: :: JGRAPH_2:22

for X, Y, Z being non empty TopSpace
for B being Subset of Y
for C being Subset of Z
for f being Function of X,Y
for h being Function of (Y | B),(Z | C) st f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} holds
ex g being Function of X,Z st
( g is continuous & g = h * f )

proof end;

definition

func Out_In_Sq -> Function of the carrier of (TOP-REAL 2) \ {(0.REAL 2)},the carrier of (TOP-REAL 2) \ {(0.REAL 2)} means :Def1: :: JGRAPH_2:def 1
for p being Point of (TOP-REAL 2) st p <> 0.REAL 2 holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies it . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or it . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Out_In_Sq JGRAPH_2:def 1 :

theorem Th23: :: JGRAPH_2:23

for p being Point of (TOP-REAL 2) holds
( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) )

proof end;

theorem Th24: :: JGRAPH_2:24

for p being Point of (TOP-REAL 2) st p <> 0.REAL 2 holds
( ( ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) implies Out_In_Sq . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) & ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) or Out_In_Sq . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) )

proof end;

theorem Th25: :: JGRAPH_2:25

for D being Subset of (TOP-REAL 2)
for K0 being Subset of ((TOP-REAL 2) | D) st 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.REAL 2 ) } holds
rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

proof end;

theorem Th26: :: JGRAPH_2:26

for D being Subset of (TOP-REAL 2)
for K0 being Subset of ((TOP-REAL 2) | D) st 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.REAL 2 ) } holds
rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

proof end;

theorem Th27: :: JGRAPH_2:27

for K0a being set
for D being non empty Subset of (TOP-REAL 2) st K0a = { 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.REAL 2 ) } & D ` = {(0.REAL 2)} holds
( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )

proof end;

theorem Th28: :: JGRAPH_2:28

for K0a being set
for D being non empty Subset of (TOP-REAL 2) st K0a = { 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.REAL 2 ) } & D ` = {(0.REAL 2)} holds
( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )

proof end;

theorem Th29: :: JGRAPH_2:29

for X being non empty TopSpace
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being real number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous )

proof end;

theorem :: JGRAPH_2:30

for X being non empty TopSpace
for a being real number ex g being Function of X,R^1 st
( ( for p being Point of X holds g . p = a ) & g is continuous )

proof end;

theorem Th31: :: JGRAPH_2:31

proof end;

theorem Th32: :: JGRAPH_2:32

for X being non empty TopSpace
for f1 being Function of X,R^1 st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = r1 * r1 ) & g is continuous )

proof end;

theorem Th33: :: JGRAPH_2:33

for X being non empty TopSpace
for f1 being Function of X,R^1
for a being real number st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = a * r1 ) & g is continuous )

proof end;

theorem Th34: :: JGRAPH_2:34

proof end;

theorem Th35: :: JGRAPH_2:35

proof end;

theorem Th36: :: JGRAPH_2:36

for X being non empty TopSpace
for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X holds f1 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = 1 / r1 ) & g is continuous )

proof end;

theorem Th37: :: JGRAPH_2:37

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 number st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 / r2 ) & g is continuous )

proof end;

theorem Th38: :: JGRAPH_2:38

proof end;

theorem Th39: :: JGRAPH_2:39

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

proof end;

theorem Th40: :: JGRAPH_2:40

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

proof end;

theorem Th41: :: JGRAPH_2:41

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 = 1 / (p `1 ) ) & ( 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 Th42: :: JGRAPH_2:42

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 = 1 / (p `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 Th43: :: JGRAPH_2:43

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 ) / (p `1 )) / (p `1 ) ) & ( 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 Th44: :: JGRAPH_2:44

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 ) / (p `2 )) / (p `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 Th45: :: JGRAPH_2:45

for K0, B0 being Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0)
for f1, f2 being Function of ((TOP-REAL 2) | K0),R^1 st f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being real number st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) holds
f is continuous

proof end;

theorem Th46: :: JGRAPH_2:46

for K0, B0 being Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = the carrier of (TOP-REAL 2) \ {(0.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.REAL 2 ) } holds
f is continuous

proof end;

theorem Th47: :: JGRAPH_2:47

for K0, B0 being Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = the carrier of (TOP-REAL 2) \ {(0.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.REAL 2 ) } holds
f is continuous

proof end;

scheme :: JGRAPH_2:sch 1
TopSubset{ P₁[ set ] } :

{ p where p is Point of (TOP-REAL 2) : P₁[p] } is Subset of (TOP-REAL 2)

proof end;

scheme :: JGRAPH_2:sch 2
TopCompl{ P₁[ set ], F₁() -> Subset of (TOP-REAL 2) } :

F₁() ` = { p where p is Point of (TOP-REAL 2) : P₁[p] }

provided

A1: F₁() = { p where p is Point of (TOP-REAL 2) : P₁[p] }

proof end;

Lm2: now

let p01, p02, px1, px2 be real number ; :: thesis:
set r0 = (p01 - p02) / 4;
assume (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) ; :: thesis:
then (p01 - p02) - (px1 - px2) <= ((p01 - p02) / 4) + ((p01 - p02) / 4) ;
then p01 - p02 <= (px1 - px2) + (((p01 - p02) / 4) + ((p01 - p02) / 4)) by XREAL_1:22;
then (p01 - p02) - ((p01 - p02) / 2) <= px1 - px2 by XREAL_1:22;
hence (p01 - p02) / 2 <= px1 - px2 ; :: thesis:

end;

scheme :: JGRAPH_2:sch 3
ClosedSubset{ F₁( Point of (TOP-REAL 2)) -> real number , F₂( Point of (TOP-REAL 2)) -> real number } :

{ p where p is Point of (TOP-REAL 2) : F₁(p) <= F₂(p) } is closed Subset of (TOP-REAL 2)

provided

A1: for p, q being Point of (TOP-REAL 2) holds
( F₁((p - q)) = F₁(p) - F₁(q) & F₂((p - q)) = F₂(p) - F₂(q) ) and
A2: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (F₁((p - q)) ^2 ) + (F₂((p - q)) ^2 )

proof end;

deffunc H₁( Point of (TOP-REAL 2)) -> Element of REAL = $1 `1 ;

deffunc H₂( Point of (TOP-REAL 2)) -> Element of REAL = $1 `2 ;

Lm3: for p, q being Point of (TOP-REAL 2) holds
( H₁(p - q) = H₁(p) - H₁(q) & H₂(p - q) = H₂(p) - H₂(q) )
by TOPREAL3:8;

Lm4: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H₁(p - q) ^2 ) + (H₂(p - q) ^2 )
by JGRAPH_1:46;

Lm5: { p7 where p7 is Point of (TOP-REAL 2) : H₁(p7) <= H₂(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(, Lm3, Lm4);

Lm6: for p, q being Point of (TOP-REAL 2) holds
( H₂(p - q) = H₂(p) - H₂(q) & H₁(p - q) = H₁(p) - H₁(q) )
by TOPREAL3:8;

Lm7: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H₂(p - q) ^2 ) + (H₁(p - q) ^2 )
by JGRAPH_1:46;

Lm8: { p7 where p7 is Point of (TOP-REAL 2) : H₂(p7) <= H₁(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(, Lm6, Lm7);

deffunc H₃( Point of (TOP-REAL 2)) -> Element of REAL = - ($1 `1 );

deffunc H₄( Point of (TOP-REAL 2)) -> Element of REAL = - ($1 `2 );

Lm9: now

let p, q be Point of (TOP-REAL 2); :: thesis:
thus H₃(p - q) = - ((p `1 ) - (q `1 )) by TOPREAL3:8
.= H₃(p) - H₃(q) ; :: thesis:
thus H₂(p - q) = H₂(p) - H₂(q) by TOPREAL3:8; :: thesis:

end;

Lm10: now

let p, q be Point of (TOP-REAL 2); :: thesis:
H₃(p - q) ^2 = H₁(p - q) ^2 ;
hence |.(p - q).| ^2 = (H₃(p - q) ^2 ) + (H₂(p - q) ^2 ) by JGRAPH_1:46; :: thesis:

end;

Lm11: { p7 where p7 is Point of (TOP-REAL 2) : H₃(p7) <= H₂(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(, Lm9, Lm10);

Lm12: now

let p, q be Point of (TOP-REAL 2); :: thesis:
thus H₂(p - q) = H₂(p) - H₂(q) by TOPREAL3:8; :: thesis:
thus H₃(p - q) = - ((p `1 ) - (q `1 )) by TOPREAL3:8
.= H₃(p) - H₃(q) ; :: thesis:

end;

Lm13: now

let p, q be Point of (TOP-REAL 2); :: thesis:
(- ((p - q) `1 )) ^2 = ((p - q) `1 ) ^2 ;
hence |.(p - q).| ^2 = (H₂(p - q) ^2 ) + (H₃(p - q) ^2 ) by JGRAPH_1:46; :: thesis:

end;

Lm14: { p7 where p7 is Point of (TOP-REAL 2) : H₂(p7) <= H₃(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(, Lm12, Lm13);

Lm15: now

let p, q be Point of (TOP-REAL 2); :: thesis:
thus H₄(p - q) = - ((p `2 ) - (q `2 )) by TOPREAL3:8
.= H₄(p) - H₄(q) ; :: thesis:
thus H₁(p - q) = H₁(p) - H₁(q) by TOPREAL3:8; :: thesis:

end;

Lm16: now

let p, q be Point of (TOP-REAL 2); :: thesis:
(- ((p - q) `2 )) ^2 = ((p - q) `2 ) ^2 ;
hence |.(p - q).| ^2 = (H₄(p - q) ^2 ) + (H₁(p - q) ^2 ) by JGRAPH_1:46; :: thesis:

end;

Lm17: { p7 where p7 is Point of (TOP-REAL 2) : H₄(p7) <= H₁(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(, Lm15, Lm16);

Lm18: now

let p, q be Point of (TOP-REAL 2); :: thesis:
thus H₁(p - q) = H₁(p) - H₁(q) by TOPREAL3:8; :: thesis:
thus H₄(p - q) = - ((p `2 ) - (q `2 )) by TOPREAL3:8
.= H₄(p) - H₄(q) ; :: thesis:

end;

Lm19: now

let p, q be Point of (TOP-REAL 2); :: thesis:
H₄(p - q) ^2 = H₂(p - q) ^2 ;
hence |.(p - q).| ^2 = (H₁(p - q) ^2 ) + (H₄(p - q) ^2 ) by JGRAPH_1:46; :: thesis:

end;

Lm20: { p7 where p7 is Point of (TOP-REAL 2) : H₁(p7) <= H₄(p7) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(, Lm18, Lm19);

theorem Th48: :: JGRAPH_2:48

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 = Out_In_Sq | K0 & B0 = the carrier of (TOP-REAL 2) \ {(0.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.REAL 2 ) } holds
( f is continuous & K0 is closed )

proof end;

theorem Th49: :: JGRAPH_2:49

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 = Out_In_Sq | K0 & B0 = the carrier of (TOP-REAL 2) \ {(0.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.REAL 2 ) } holds
( f is continuous & K0 is closed )

proof end;

theorem Th50: :: JGRAPH_2:50

for D being non empty Subset of (TOP-REAL 2) st D ` = {(0.REAL 2)} holds
ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Out_In_Sq & h is continuous )

proof end;

theorem Th51: :: JGRAPH_2:51

for B, K0, Kb being Subset of (TOP-REAL 2) st B = {(0.REAL 2)} & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & 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
ex f being Function of ((TOP-REAL 2) | (B ` )),((TOP-REAL 2) | (B ` )) st
( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0.REAL 2 holds
not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds
f . s = s ) )

proof end;

theorem Th52: :: JGRAPH_2:52

for f, g being Function of I[01] ,(TOP-REAL 2)
for K0 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 & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & (f . O) `1 = - 1 & (f . I) `1 = 1 & - 1 <= (f . O) `2 & (f . O) `2 <= 1 & - 1 <= (f . I) `2 & (f . I) `2 <= 1 & (g . O) `2 = - 1 & (g . I) `2 = 1 & - 1 <= (g . O) `1 & (g . O) `1 <= 1 & - 1 <= (g . I) `1 & (g . I) `1 <= 1 & rng f misses K0 & rng g misses K0 holds
rng f meets rng g

proof end;

theorem Th53: :: JGRAPH_2:53

for A, B, C, D being real number
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for t being Point of (TOP-REAL 2) holds f . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]| ) holds
f is continuous

proof end;

definition

let A, B, C, D be real number ;
func AffineMap A,B,C,D -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def2: :: JGRAPH_2:def 2
for t being Point of (TOP-REAL 2) holds it . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines AffineMap JGRAPH_2:def 2 :

registration

let a, b, c, d be real number ;
cluster AffineMap a,b,c,d -> continuous ;
coherence

proof end;

end;

theorem Th54: :: JGRAPH_2:54

for A, B, C, D being real number st A > 0 & C > 0 holds
AffineMap A,B,C,D is one-to-one

proof end;

theorem :: JGRAPH_2:55

for f, g being Function of I[01] ,(TOP-REAL 2)
for a, b, c, d being real number
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 & (f . O) `1 = a & (f . I) `1 = b & c <= (f . O) `2 & (f . O) `2 <= d & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & (g . I) `2 = d & a <= (g . O) `1 & (g . O) `1 <= b & a <= (g . I) `1 & (g . I) `1 <= b & a < b & c < d & ( for r being Point of I[01] holds
( not a < (f . r) `1 or not (f . r) `1 < b or not c < (f . r) `2 or not (f . r) `2 < d ) ) & ( for r being Point of I[01] holds
( not a < (g . r) `1 or not (g . r) `1 < b or not c < (g . r) `2 or not (g . r) `2 < d ) ) holds
rng f meets rng g

proof end;

theorem :: JGRAPH_2:56

( { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= p7 `1 } is closed Subset of (TOP-REAL 2) & { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= p7 `2 } is closed Subset of (TOP-REAL 2) ) by Lm5, Lm8;

theorem :: JGRAPH_2:57

( { p7 where p7 is Point of (TOP-REAL 2) : - (p7 `1 ) <= p7 `2 } is closed Subset of (TOP-REAL 2) & { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= - (p7 `1 ) } is closed Subset of (TOP-REAL 2) ) by Lm11, Lm14;

theorem :: JGRAPH_2:58

( { p7 where p7 is Point of (TOP-REAL 2) : - (p7 `2 ) <= p7 `1 } is closed Subset of (TOP-REAL 2) & { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= - (p7 `2 ) } is closed Subset of (TOP-REAL 2) ) by Lm17, Lm20;