for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₂
for b₇, b₈ being Subset of b₄ st b₁ is SubSpace of b₄ & b₃ is SubSpace of b₄ & b₇ = [#] b₁ & b₈ = [#] b₃ & ([#] b₁) \/ ([#] b₃) = [#] b₄ & b₇ is closed & b₈ is closed & b₅ is continuous & b₆ is continuous & ( for b₉ being set st b₉ in ([#] b₁) /\ ([#] b₃) holds
b₅ . b₉ = b₆ . b₉ ) holds
ex b₉ being Function of b₄,b₂ st
( b₉ = b₅ +* b₆ & b₉ is continuous )

proof end;

theorem Th10: :: JGRAPH_2:10

for b₁ being Nat
for b₂ being Point of (Euclid b₁)
for b₃ being Point of (TOP-REAL b₁)
for b₄ being real number st b₃ = b₂ holds
Ball b₂,b₄ = { b₅ where B is Point of (TOP-REAL b₁) : |.(b₃ - b₅).| < b₄ }

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 Th16: :: JGRAPH_2:16

canceled;

theorem Th17: :: JGRAPH_2:17

canceled;

theorem Th18: :: JGRAPH_2:18

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

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 b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ holds
( b₃ is continuous iff for b₄ being Point of b₁
for b₅ being Subset of b₂ st b₃ . b₄ in b₅ & b₅ is open holds
ex b₆ being Subset of b₁ st
( b₄ in b₆ & b₆ is open & b₃ .: b₆ c= b₅ ) )

proof end;

theorem Th21: :: JGRAPH_2:21

for b₁ being Point of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) st b₂ is open & b₁ in b₂ holds
ex b₃ being real number st
( b₃ > 0 & { b₄ where B is Point of (TOP-REAL 2) : ( (b₁ `1 ) - b₃ < b₄ `1 & b₄ `1 < (b₁ `1 ) + b₃ & (b₁ `2 ) - b₃ < b₄ `2 & b₄ `2 < (b₁ `2 ) + b₃ ) } c= b₂ )

proof end;

theorem Th22: :: JGRAPH_2:22

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being Subset of b₂
for b₅ being Subset of b₃
for b₆ being Function of b₁,b₂
for b₇ being Function of (b₂ | b₄),(b₃ | b₅) st b₆ is continuous & b₇ is continuous & rng b₆ c= b₄ & b₄ <> {} & b₅ <> {} holds
ex b₈ being Function of b₁,b₃ st
( b₈ is continuous & b₈ = b₇ * b₆ )

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 b₁ being Point of (TOP-REAL 2) st b₁ <> 0.REAL 2 holds
( ( ( ( b₁ `2 <= b₁ `1 & - (b₁ `1 ) <= b₁ `2 ) or ( b₁ `2 >= b₁ `1 & b₁ `2 <= - (b₁ `1 ) ) ) implies a₁ . b₁ = |[(1 / (b₁ `1 )),(((b₁ `2 ) / (b₁ `1 )) / (b₁ `1 ))]| ) & ( ( b₁ `2 <= b₁ `1 & - (b₁ `1 ) <= b₁ `2 ) or ( b₁ `2 >= b₁ `1 & b₁ `2 <= - (b₁ `1 ) ) or a₁ . b₁ = |[(((b₁ `1 ) / (b₁ `2 )) / (b₁ `2 )),(1 / (b₁ `2 ))]| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Out_In_Sq JGRAPH_2:def 1 :

theorem Th23: :: JGRAPH_2:23

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

proof end;

theorem Th24: :: JGRAPH_2:24

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

proof end;

theorem Th25: :: JGRAPH_2:25

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

proof end;

theorem Th26: :: JGRAPH_2:26

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

proof end;

theorem Th27: :: JGRAPH_2:27

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

proof end;

theorem Th28: :: JGRAPH_2:28

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

proof end;

theorem Th29: :: JGRAPH_2:29

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

proof end;

theorem Th30: :: JGRAPH_2:30

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

proof end;

theorem Th31: :: JGRAPH_2:31

proof end;

theorem Th32: :: JGRAPH_2:32

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

proof end;

theorem Th33: :: JGRAPH_2:33

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

proof end;

theorem Th34: :: JGRAPH_2:34

proof end;

theorem Th35: :: JGRAPH_2:35

proof end;

theorem Th36: :: JGRAPH_2:36

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

proof end;

theorem Th37: :: JGRAPH_2:37

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

proof end;

theorem Th38: :: JGRAPH_2:38

proof end;

theorem Th39: :: JGRAPH_2:39

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

proof end;

theorem Th40: :: JGRAPH_2:40

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

proof end;

theorem Th41: :: JGRAPH_2:41

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

proof end;

theorem Th42: :: JGRAPH_2:42

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

proof end;

theorem Th43: :: JGRAPH_2:43

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

proof end;

theorem Th44: :: JGRAPH_2:44

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

proof end;

theorem Th45: :: JGRAPH_2:45

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃ being Function of ((TOP-REAL 2) | b₁),((TOP-REAL 2) | b₂)
for b₄, b₅ being Function of ((TOP-REAL 2) | b₁),R^1 st b₄ is continuous & b₅ is continuous & b₁ <> {} & b₂ <> {} & ( for b₆, b₇, b₈, b₉ being real number st |[b₆,b₇]| in b₁ & b₈ = b₄ . |[b₆,b₇]| & b₉ = b₅ . |[b₆,b₇]| holds
b₃ . |[b₆,b₇]| = |[b₈,b₉]| ) holds
b₃ is continuous

proof end;

theorem Th46: :: JGRAPH_2:46

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

proof end;

theorem Th47: :: JGRAPH_2:47

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

proof end;

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

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

proof end;

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

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

provided

E44: F₁() = { b₁ where B is Point of (TOP-REAL 2) : P₁[b₁] }

proof end;

E44: now

let c₁, c₂, c₃, c₄ be real number ;
set c₅ = (c₁ - c₂) / 4;
assume (c₁ - c₃) - (c₂ - c₄) <= ((c₁ - c₂) / 4) - (- ((c₁ - c₂) / 4)) ;
then (c₁ - c₂) - (c₃ - c₄) <= ((c₁ - c₂) / 4) + ((c₁ - c₂) / 4) ;
then c₁ - c₂ <= (c₃ - c₄) + (((c₁ - c₂) / 4) + ((c₁ - c₂) / 4)) by XREAL_1:22;
then (c₁ - c₂) - ((c₁ - c₂) / 2) <= c₃ - c₄ by XREAL_1:22;
hence (c₁ - c₂) / 2 <= c₃ - c₄ ;

end;

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

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

provided

E45: for b₁, b₂ being Point of (TOP-REAL 2) holds
( F₁((b₁ - b₂)) = F₁(b₁) - F₁(b₂) & F₂((b₁ - b₂)) = F₂(b₁) - F₂(b₂) ) and
E46: for b₁, b₂ being Point of (TOP-REAL 2) holds |.(b₁ - b₂).| ^2 = (F₁((b₁ - b₂)) ^2 ) + (F₂((b₁ - b₂)) ^2 )

proof end;

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

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

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

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

Lemma47: { b₁ where B is Point of (TOP-REAL 2) : H₁(b₁) <= H₂(b₁) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lemma45, Lemma46);

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

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

Lemma50: { b₁ where B is Point of (TOP-REAL 2) : H₂(b₁) <= H₁(b₁) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lemma48, Lemma49);

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

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

E51: now

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

end;

E52: now

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

end;

Lemma53: { b₁ where B is Point of (TOP-REAL 2) : H₃(b₁) <= H₂(b₁) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lemma51, Lemma52);

E54: now

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

end;

E55: now

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

end;

Lemma56: { b₁ where B is Point of (TOP-REAL 2) : H₂(b₁) <= H₃(b₁) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lemma54, Lemma55);

E57: now

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

end;

E58: now

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

end;

Lemma59: { b₁ where B is Point of (TOP-REAL 2) : H₄(b₁) <= H₁(b₁) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lemma57, Lemma58);

E60: now

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

end;

E61: now

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

end;

Lemma62: { b₁ where B is Point of (TOP-REAL 2) : H₁(b₁) <= H₄(b₁) } is closed Subset of (TOP-REAL 2)
from JGRAPH_2:sch 3(Lemma60, Lemma61);

theorem Th48: :: JGRAPH_2:48

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

proof end;

theorem Th49: :: JGRAPH_2:49

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

proof end;

theorem Th50: :: JGRAPH_2:50

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

proof end;

theorem Th51: :: JGRAPH_2:51

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

proof end;

theorem Th52: :: JGRAPH_2:52

for b₁, b₂ being Function of I[01] ,(TOP-REAL 2)
for b₃ being Subset of (TOP-REAL 2)
for b₄, b₅ being Point of I[01] st b₄ = 0 & b₅ = 1 & b₁ is continuous & b₁ is one-to-one & b₂ is continuous & b₂ is one-to-one & b₃ = { b₆ where B is Point of (TOP-REAL 2) : ( - 1 < b₆ `1 & b₆ `1 < 1 & - 1 < b₆ `2 & b₆ `2 < 1 ) } & (b₁ . b₄) `1 = - 1 & (b₁ . b₅) `1 = 1 & - 1 <= (b₁ . b₄) `2 & (b₁ . b₄) `2 <= 1 & - 1 <= (b₁ . b₅) `2 & (b₁ . b₅) `2 <= 1 & (b₂ . b₄) `2 = - 1 & (b₂ . b₅) `2 = 1 & - 1 <= (b₂ . b₄) `1 & (b₂ . b₄) `1 <= 1 & - 1 <= (b₂ . b₅) `1 & (b₂ . b₅) `1 <= 1 & rng b₁ misses b₃ & rng b₂ misses b₃ holds
rng b₁ meets rng b₂

proof end;

theorem Th53: :: JGRAPH_2:53

for b₁, b₂, b₃, b₄ being real number
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for b₆ being Point of (TOP-REAL 2) holds b₅ . b₆ = |[((b₁ * (b₆ `1 )) + b₂),((b₃ * (b₆ `2 )) + b₄)]| ) holds
b₅ is continuous

proof end;

definition

let c₁, c₂, c₃, c₄ be real number ;
func AffineMap c₁,c₂,c₃,c₄ -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def2: :: JGRAPH_2:def 2
for b₁ being Point of (TOP-REAL 2) holds a₅ . b₁ = |[((a₁ * (b₁ `1 )) + a₂),((a₃ * (b₁ `2 )) + a₄)]|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines AffineMap JGRAPH_2:def 2 :

registration

let c₁, c₂, c₃, c₄ be real number ;
cluster AffineMap a₁,a₂,a₃,a₄ -> continuous ;
coherence

proof end;

end;

theorem Th54: :: JGRAPH_2:54

for b₁, b₂, b₃, b₄ being real number st b₁ > 0 & b₃ > 0 holds
AffineMap b₁,b₂,b₃,b₄ is one-to-one

proof end;

theorem Th55: :: JGRAPH_2:55

for b₁, b₂ being Function of I[01] ,(TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number
for b₇, b₈ being Point of I[01] st b₇ = 0 & b₈ = 1 & b₁ is continuous & b₁ is one-to-one & b₂ is continuous & b₂ is one-to-one & (b₁ . b₇) `1 = b₃ & (b₁ . b₈) `1 = b₄ & b₅ <= (b₁ . b₇) `2 & (b₁ . b₇) `2 <= b₆ & b₅ <= (b₁ . b₈) `2 & (b₁ . b₈) `2 <= b₆ & (b₂ . b₇) `2 = b₅ & (b₂ . b₈) `2 = b₆ & b₃ <= (b₂ . b₇) `1 & (b₂ . b₇) `1 <= b₄ & b₃ <= (b₂ . b₈) `1 & (b₂ . b₈) `1 <= b₄ & b₃ < b₄ & b₅ < b₆ & ( for b₉ being Point of I[01] holds
( not b₃ < (b₁ . b₉) `1 or not (b₁ . b₉) `1 < b₄ or not b₅ < (b₁ . b₉) `2 or not (b₁ . b₉) `2 < b₆ ) ) & ( for b₉ being Point of I[01] holds
( not b₃ < (b₂ . b₉) `1 or not (b₂ . b₉) `1 < b₄ or not b₅ < (b₂ . b₉) `2 or not (b₂ . b₉) `2 < b₆ ) ) holds
rng b₁ meets rng b₂

proof end;

theorem Th56: :: JGRAPH_2:56

( { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 <= b₁ `1 } is closed Subset of (TOP-REAL 2) & { b₁ where B is Point of (TOP-REAL 2) : b₁ `1 <= b₁ `2 } is closed Subset of (TOP-REAL 2) ) by Lemma47, Lemma50;

theorem Th57: :: JGRAPH_2:57

( { b₁ where B is Point of (TOP-REAL 2) : - (b₁ `1 ) <= b₁ `2 } is closed Subset of (TOP-REAL 2) & { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 <= - (b₁ `1 ) } is closed Subset of (TOP-REAL 2) ) by Lemma53, Lemma56;

theorem Th58: :: JGRAPH_2:58

( { b₁ where B is Point of (TOP-REAL 2) : - (b₁ `2 ) <= b₁ `1 } is closed Subset of (TOP-REAL 2) & { b₁ where B is Point of (TOP-REAL 2) : b₁ `1 <= - (b₁ `2 ) } is closed Subset of (TOP-REAL 2) ) by Lemma59, Lemma62;