:: On Outside Fashoda Meet Theorem
:: by Yatsuka Nakamura
::
:: Copyright (c) 2001-2021 Association of Mizar Users

theorem Th1: :: JGRAPH_2:1
for T, T1, T2, S 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 object 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 Th2: :: JGRAPH_2:2
for n being Element of NAT
for q2 being Point of ()
for q being Point of ()
for r being Real st q = q2 holds
Ball (q2,r) = { q3 where q3 is Point of () : |.(q - q3).| < r }
proof end;

theorem Th3: :: JGRAPH_2:3
( (0. ()) 1 = 0 & (0. ()) 2 = 0 ) by ;

theorem Th4: :: JGRAPH_2:4
1.REAL 2 = <*1,1*> by FINSEQ_2:61;

theorem Th5: :: JGRAPH_2:5
( () 1 = 1 & () 2 = 1 ) by ;

theorem Th6: :: JGRAPH_2:6
( dom proj1 = the carrier of () & dom proj1 = REAL 2 )
proof end;

theorem Th7: :: JGRAPH_2:7
( dom proj2 = the carrier of () & dom proj2 = REAL 2 )
proof end;

theorem Th8: :: JGRAPH_2:8
for p being Point of () holds p = |[(),()]|
proof end;

theorem Th9: :: JGRAPH_2:9
for B being Subset of () st B = {(0. ())} holds
( B  <> {} & the carrier of () \ B <> {} )
proof end;

theorem Th10: :: JGRAPH_2:10
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 Th11: :: JGRAPH_2:11
for p being Point of ()
for G being Subset of () st G is open & p in G holds
ex r being Real st
( r > 0 & { q where q is Point of () : ( (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 Th12: :: JGRAPH_2:12
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 (NonZero ()),(NonZero ()) means :Def1: :: JGRAPH_2:def 1
for p being Point of () st p <> 0. () 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
ex b1 being Function of (NonZero ()),(NonZero ()) st
for p being Point of () st p <> 0. () holds
( ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) implies b1 . 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 b1 . p = |[(((p 1) / (p 2)) / (p 2)),(1 / (p 2))]| ) )
proof end;
uniqueness
for b1, b2 being Function of (NonZero ()),(NonZero ()) st ( for p being Point of () st p <> 0. () holds
( ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) implies b1 . 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 b1 . p = |[(((p 1) / (p 2)) / (p 2)),(1 / (p 2))]| ) ) ) & ( for p being Point of () st p <> 0. () holds
( ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) implies b2 . 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 b2 . p = |[(((p 1) / (p 2)) / (p 2)),(1 / (p 2))]| ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Out_In_Sq JGRAPH_2:def 1 :
for b1 being Function of (NonZero ()),(NonZero ()) holds
( b1 = Out_In_Sq iff for p being Point of () st p <> 0. () holds
( ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) implies b1 . 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 b1 . p = |[(((p 1) / (p 2)) / (p 2)),(1 / (p 2))]| ) ) );

theorem Th13: :: JGRAPH_2:13
for p being Point of () 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 Th14: :: JGRAPH_2:14
for p being Point of () st p <> 0. () 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 Th15: :: JGRAPH_2:15
for D being Subset of ()
for K0 being Subset of (() | D) st K0 = { p where p is Point of () : ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () ) } holds
rng () c= the carrier of ((() | D) | K0)
proof end;

theorem Th16: :: JGRAPH_2:16
for D being Subset of ()
for K0 being Subset of (() | D) st K0 = { p where p is Point of () : ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) & p <> 0. () ) } holds
rng () c= the carrier of ((() | D) | K0)
proof end;

Lm1: 0. () = 0.REAL 2
by EUCLID:66;

theorem Th17: :: JGRAPH_2:17
for K0a being set
for D being non empty Subset of () st K0a = { p where p is Point of () : ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () ) } & D  = {(0. ())} holds
( K0a is non empty Subset of (() | D) & K0a is non empty Subset of () )
proof end;

theorem Th18: :: JGRAPH_2:18
for K0a being set
for D being non empty Subset of () st K0a = { p where p is Point of () : ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) & p <> 0. () ) } & D  = {(0. ())} holds
( K0a is non empty Subset of (() | D) & K0a is non empty Subset of () )
proof end;

theorem Th19: :: JGRAPH_2:19
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 st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous )
proof end;

theorem :: JGRAPH_2:20
for X being non empty TopSpace
for a being Real 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 Th21: :: JGRAPH_2:21
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 st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 - r2 ) & g is continuous )
proof end;

theorem Th22: :: JGRAPH_2:22
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 st f1 . p = r1 holds
g . p = r1 * r1 ) & g is continuous )
proof end;

theorem Th23: :: JGRAPH_2:23
for X being non empty TopSpace
for f1 being Function of X,R^1
for a being Real st f1 is continuous 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 = a * r1 ) & g is continuous )
proof end;

theorem Th24: :: JGRAPH_2:24
for X being non empty TopSpace
for f1 being Function of X,R^1
for a being Real st f1 is continuous 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 = r1 + a ) & g is continuous )
proof end;

theorem Th25: :: JGRAPH_2:25
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 st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * r2 ) & g is continuous )
proof end;

theorem Th26: :: JGRAPH_2:26
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 st f1 . p = r1 holds
g . p = 1 / r1 ) & g is continuous )
proof end;

theorem Th27: :: JGRAPH_2:27
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 ) & g is continuous )
proof end;

theorem Th28: :: JGRAPH_2:28
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) / r2 ) & g is continuous )
proof end;

theorem Th29: :: JGRAPH_2:29
for K0 being Subset of ()
for f being Function of (() | K0),R^1 st ( for p being Point of (() | K0) holds f . p = proj1 . p ) holds
f is continuous
proof end;

theorem Th30: :: JGRAPH_2:30
for K0 being Subset of ()
for f being Function of (() | K0),R^1 st ( for p being Point of (() | K0) holds f . p = proj2 . p ) holds
f is continuous
proof end;

theorem Th31: :: JGRAPH_2:31
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = 1 / (p 1) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 1 <> 0 ) holds
f is continuous
proof end;

theorem Th32: :: JGRAPH_2:32
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = 1 / (p 2) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 2 <> 0 ) holds
f is continuous
proof end;

theorem Th33: :: JGRAPH_2:33
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = ((p 2) / (p 1)) / (p 1) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 1 <> 0 ) holds
f is continuous
proof end;

theorem Th34: :: JGRAPH_2:34
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = ((p 1) / (p 2)) / (p 2) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 2 <> 0 ) holds
f is continuous
proof end;

theorem Th35: :: JGRAPH_2:35
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0)
for f1, f2 being Function of (() | K0),R^1 st f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being Real 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 Th36: :: JGRAPH_2:36
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st f = Out_In_Sq | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th37: :: JGRAPH_2:37
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st f = Out_In_Sq | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) & p <> 0. () ) } holds
f is continuous
proof end;

scheme :: JGRAPH_2:sch 1
TopSubset{ P1[ set ] } :
{ p where p is Point of () : P1[p] } is Subset of ()
proof end;

scheme :: JGRAPH_2:sch 2
TopCompl{ P1[ set ], F1() -> Subset of () } :
F1()  = { p where p is Point of () : P1[p] }
provided
A1: F1() = { p where p is Point of () : P1[p] }
proof end;

Lm2: now :: thesis: for p01, p02, px1, px2 being Real st (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) holds
(p01 - p02) / 2 <= px1 - px2
let p01, p02, px1, px2 be Real; :: thesis: ( (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) implies (p01 - p02) / 2 <= px1 - px2 )
set r0 = (p01 - p02) / 4;
assume (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) ; :: thesis: (p01 - p02) / 2 <= px1 - px2
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:20;
then (p01 - p02) - ((p01 - p02) / 2) <= px1 - px2 by XREAL_1:20;
hence (p01 - p02) / 2 <= px1 - px2 ; :: thesis: verum
end;

scheme :: JGRAPH_2:sch 3
ClosedSubset{ F1( Point of ()) -> Real, F2( Point of ()) -> Real } :
{ p where p is Point of () : F1(p) <= F2(p) } is closed Subset of ()
provided
A1: for p, q being Point of () holds
( F1((p - q)) = F1(p) - F1(q) & F2((p - q)) = F2(p) - F2(q) ) and
A2: for p, q being Point of () holds |.(p - q).| ^2 = (F1((p - q)) ^2) + (F2((p - q)) ^2)
proof end;

deffunc H1( Point of ()) -> object = $1 1 ; deffunc H2( Point of ()) -> object =$1 2 ;

Lm3: for p, q being Point of () holds
( H1(p - q) = H1(p) - H1(q) & H2(p - q) = H2(p) - H2(q) )

by TOPREAL3:3;

Lm4: for p, q being Point of () holds |.(p - q).| ^2 = (H1(p - q) ^2) + (H2(p - q) ^2)
by JGRAPH_1:29;

Lm5: { p7 where p7 is Point of () : H1(p7) <= H2(p7) } is closed Subset of ()
from
Lm6: for p, q being Point of () holds
( H2(p - q) = H2(p) - H2(q) & H1(p - q) = H1(p) - H1(q) )

by TOPREAL3:3;

Lm7: for p, q being Point of () holds |.(p - q).| ^2 = (H2(p - q) ^2) + (H1(p - q) ^2)
by JGRAPH_1:29;

Lm8: { p7 where p7 is Point of () : H2(p7) <= H1(p7) } is closed Subset of ()
from
deffunc H3( Point of ()) -> object = - ($1 1); deffunc H4( Point of ()) -> object = - ($1 2);

Lm9: now :: thesis: for p, q being Point of () holds
( H3(p - q) = H3(p) - H3(q) & H2(p - q) = H2(p) - H2(q) )
let p, q be Point of (); :: thesis: ( H3(p - q) = H3(p) - H3(q) & H2(p - q) = H2(p) - H2(q) )
thus H3(p - q) = - ((p 1) - (q 1)) by TOPREAL3:3
.= H3(p) - H3(q) ; :: thesis: H2(p - q) = H2(p) - H2(q)
thus H2(p - q) = H2(p) - H2(q) by TOPREAL3:3; :: thesis: verum
end;

Lm10: now :: thesis: for p, q being Point of () holds |.(p - q).| ^2 = (H3(p - q) ^2) + (H2(p - q) ^2)
let p, q be Point of (); :: thesis: |.(p - q).| ^2 = (H3(p - q) ^2) + (H2(p - q) ^2)
H3(p - q) ^2 = H1(p - q) ^2 ;
hence |.(p - q).| ^2 = (H3(p - q) ^2) + (H2(p - q) ^2) by JGRAPH_1:29; :: thesis: verum
end;

Lm11: { p7 where p7 is Point of () : H3(p7) <= H2(p7) } is closed Subset of ()
from
Lm12: now :: thesis: for p, q being Point of () holds
( H2(p - q) = H2(p) - H2(q) & H3(p - q) = H3(p) - H3(q) )
let p, q be Point of (); :: thesis: ( H2(p - q) = H2(p) - H2(q) & H3(p - q) = H3(p) - H3(q) )
thus H2(p - q) = H2(p) - H2(q) by TOPREAL3:3; :: thesis: H3(p - q) = H3(p) - H3(q)
thus H3(p - q) = - ((p 1) - (q 1)) by TOPREAL3:3
.= H3(p) - H3(q) ; :: thesis: verum
end;

Lm13: now :: thesis: for p, q being Point of () holds |.(p - q).| ^2 = (H2(p - q) ^2) + (H3(p - q) ^2)
let p, q be Point of (); :: thesis: |.(p - q).| ^2 = (H2(p - q) ^2) + (H3(p - q) ^2)
(- ((p - q) 1)) ^2 = ((p - q) 1) ^2 ;
hence |.(p - q).| ^2 = (H2(p - q) ^2) + (H3(p - q) ^2) by JGRAPH_1:29; :: thesis: verum
end;

Lm14: { p7 where p7 is Point of () : H2(p7) <= H3(p7) } is closed Subset of ()
from
Lm15: now :: thesis: for p, q being Point of () holds
( H4(p - q) = H4(p) - H4(q) & H1(p - q) = H1(p) - H1(q) )
let p, q be Point of (); :: thesis: ( H4(p - q) = H4(p) - H4(q) & H1(p - q) = H1(p) - H1(q) )
thus H4(p - q) = - ((p 2) - (q 2)) by TOPREAL3:3
.= H4(p) - H4(q) ; :: thesis: H1(p - q) = H1(p) - H1(q)
thus H1(p - q) = H1(p) - H1(q) by TOPREAL3:3; :: thesis: verum
end;

Lm16: now :: thesis: for p, q being Point of () holds |.(p - q).| ^2 = (H4(p - q) ^2) + (H1(p - q) ^2)
let p, q be Point of (); :: thesis: |.(p - q).| ^2 = (H4(p - q) ^2) + (H1(p - q) ^2)
(- ((p - q) 2)) ^2 = ((p - q) 2) ^2 ;
hence |.(p - q).| ^2 = (H4(p - q) ^2) + (H1(p - q) ^2) by JGRAPH_1:29; :: thesis: verum
end;

Lm17: { p7 where p7 is Point of () : H4(p7) <= H1(p7) } is closed Subset of ()
from
Lm18: now :: thesis: for p, q being Point of () holds
( H1(p - q) = H1(p) - H1(q) & H4(p - q) = H4(p) - H4(q) )
let p, q be Point of (); :: thesis: ( H1(p - q) = H1(p) - H1(q) & H4(p - q) = H4(p) - H4(q) )
thus H1(p - q) = H1(p) - H1(q) by TOPREAL3:3; :: thesis: H4(p - q) = H4(p) - H4(q)
thus H4(p - q) = - ((p 2) - (q 2)) by TOPREAL3:3
.= H4(p) - H4(q) ; :: thesis: verum
end;

Lm19: now :: thesis: for p, q being Point of () holds |.(p - q).| ^2 = (H1(p - q) ^2) + (H4(p - q) ^2)
let p, q be Point of (); :: thesis: |.(p - q).| ^2 = (H1(p - q) ^2) + (H4(p - q) ^2)
H4(p - q) ^2 = H2(p - q) ^2 ;
hence |.(p - q).| ^2 = (H1(p - q) ^2) + (H4(p - q) ^2) by JGRAPH_1:29; :: thesis: verum
end;

Lm20: { p7 where p7 is Point of () : H1(p7) <= H4(p7) } is closed Subset of ()
from
theorem Th38: :: JGRAPH_2:38
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st f = Out_In_Sq | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () ) } holds
( f is continuous & K0 is closed )
proof end;

theorem Th39: :: JGRAPH_2:39
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st f = Out_In_Sq | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) & p <> 0. () ) } holds
( f is continuous & K0 is closed )
proof end;

theorem Th40: :: JGRAPH_2:40
for D being non empty Subset of () st D  = {(0. ())} holds
ex h being Function of (() | D),(() | D) st
( h = Out_In_Sq & h is continuous )
proof end;

theorem Th41: :: JGRAPH_2:41
for B, K0, Kb being Subset of () st B = {(0. ())} & K0 = { p where p is Point of () : ( - 1 < p 1 & p 1 < 1 & - 1 < p 2 & p 2 < 1 ) } & Kb = { q where q is Point of () : ( ( - 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 (() | (B )),(() | (B )) st
( f is continuous & f is one-to-one & ( for t being Point of () st t in K0 & t <> 0. () holds
not f . t in K0 \/ Kb ) & ( for r being Point of () st not r in K0 \/ Kb holds
f . r in K0 ) & ( for s being Point of () st s in Kb holds
f . s = s ) )
proof end;

theorem Th42: :: JGRAPH_2:42
for f, g being Function of I[01],()
for K0 being Subset of ()
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 () : ( - 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 Th43: :: JGRAPH_2:43
for A, B, C, D being Real
for f being Function of (),() st ( for t being Point of () 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;
func AffineMap (A,B,C,D) -> Function of (),() means :Def2: :: JGRAPH_2:def 2
for t being Point of () holds it . t = |[((A * (t 1)) + B),((C * (t 2)) + D)]|;
existence
ex b1 being Function of (),() st
for t being Point of () holds b1 . t = |[((A * (t 1)) + B),((C * (t 2)) + D)]|
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for t being Point of () holds b1 . t = |[((A * (t 1)) + B),((C * (t 2)) + D)]| ) & ( for t being Point of () holds b2 . t = |[((A * (t 1)) + B),((C * (t 2)) + D)]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines AffineMap JGRAPH_2:def 2 :
for A, B, C, D being Real
for b5 being Function of (),() holds
( b5 = AffineMap (A,B,C,D) iff for t being Point of () holds b5 . t = |[((A * (t 1)) + B),((C * (t 2)) + D)]| );

registration
let a, b, c, d be Real;
cluster AffineMap (a,b,c,d) -> continuous ;
coherence
AffineMap (a,b,c,d) is continuous
proof end;
end;

theorem Th44: :: JGRAPH_2:44
for A, B, C, D being Real st A > 0 & C > 0 holds
AffineMap (A,B,C,D) is one-to-one
proof end;

theorem :: JGRAPH_2:45
for f, g being Function of I[01],()
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 & (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:46
( { p7 where p7 is Point of () : p7 2 <= p7 1 } is closed Subset of () & { p7 where p7 is Point of () : p7 1 <= p7 2 } is closed Subset of () ) by ;

theorem :: JGRAPH_2:47
( { p7 where p7 is Point of () : - (p7 1) <= p7 2 } is closed Subset of () & { p7 where p7 is Point of () : p7 2 <= - (p7 1) } is closed Subset of () ) by ;

theorem :: JGRAPH_2:48
( { p7 where p7 is Point of () : - (p7 2) <= p7 1 } is closed Subset of () & { p7 where p7 is Point of () : p7 1 <= - (p7 `2) } is closed Subset of () ) by ;