let f, g be Function of I[01] ,(TOP-REAL 2); :: thesis: 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
let K0 be Subset of (TOP-REAL 2); :: thesis: 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
let O, I be Point of I[01] ; :: thesis: ( 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 implies rng f meets rng g )
assume A1:
( 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) /\ K0 = {} & (rng g) /\ K0 = {} )
; :: according to XBOOLE_0:def 7 :: thesis: rng f meets rng g
defpred S1[ Point of (TOP-REAL 2)] means ( ( - 1 = $1 `1 & - 1 <= $1 `2 & $1 `2 <= 1 ) or ( $1 `1 = 1 & - 1 <= $1 `2 & $1 `2 <= 1 ) or ( - 1 = $1 `2 & - 1 <= $1 `1 & $1 `1 <= 1 ) or ( 1 = $1 `2 & - 1 <= $1 `1 & $1 `1 <= 1 ) );
reconsider Kb = { q where q is Point of (TOP-REAL 2) : S1[q] } as Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
reconsider B = {(0. (TOP-REAL 2))} as Subset of (TOP-REAL 2) ;
consider h being Function of ((TOP-REAL 2) | (B ` )),((TOP-REAL 2) | (B ` )) such that
A2:
( h is continuous & h is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not h . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
h . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds
h . s = s ) )
by A1, Th51;
A3:
dom f = the carrier of I[01]
by FUNCT_2:def 1;
A4:
dom g = the carrier of I[01]
by FUNCT_2:def 1;
A5:
B ` <> {}
by Th19;
rng f c= B `
then consider w being Function of I[01] ,(TOP-REAL 2) such that
A8:
( w is continuous & w = h * f )
by A1, A2, A5, Th22;
reconsider d1 = h * f as Function of I[01] ,(TOP-REAL 2) by A8;
A9: the carrier of ((TOP-REAL 2) | (B ` )) =
[#] ((TOP-REAL 2) | (B ` ))
.=
B `
by PRE_TOPC:def 10
;
rng f c= the carrier of (TOP-REAL 2) \ B
then A12:
rng f c= the carrier of ((TOP-REAL 2) | (B ` ))
by A9, SUBSET_1:def 5;
A13:
d1 is one-to-one
by A1, A2, FUNCT_1:46;
rng g c= B `
then consider w2 being Function of I[01] ,(TOP-REAL 2) such that
A16:
( w2 is continuous & w2 = h * g )
by A1, A2, A5, Th22;
reconsider d2 = h * g as Function of I[01] ,(TOP-REAL 2) by A16;
rng g c= the carrier of (TOP-REAL 2) \ B
then A19:
rng g c= the carrier of ((TOP-REAL 2) | (B ` ))
by A9, SUBSET_1:def 5;
A20:
d2 is one-to-one
by A1, A2, FUNCT_1:46;
f . O in Kb
by A1;
then A21:
h . (f . O) = f . O
by A2;
f . I in Kb
by A1;
then A22:
h . (f . I) = f . I
by A2;
g . O in Kb
by A1;
then A23:
h . (g . O) = g . O
by A2;
g . I in Kb
by A1;
then
h . (g . I) = g . I
by A2;
then A24:
( (d1 . O) `1 = - 1 & (d1 . I) `1 = 1 & (d2 . O) `2 = - 1 & (d2 . I) `2 = 1 )
by A1, A3, A4, A21, A22, A23, FUNCT_1:23;
for r being Point of I[01] holds
( - 1 <= (d1 . r) `1 & (d1 . r) `1 <= 1 & - 1 <= (d2 . r) `1 & (d2 . r) `1 <= 1 & - 1 <= (d1 . r) `2 & (d1 . r) `2 <= 1 & - 1 <= (d2 . r) `2 & (d2 . r) `2 <= 1 )
then
rng d1 meets rng d2
by A1, A8, A13, A16, A20, A24, JGRAPH_1:65;
then A49:
(rng d1) /\ (rng d2) <> {}
by XBOOLE_0:def 7;
consider s being Element of (rng d1) /\ (rng d2);
A50:
( s in rng d1 & s in rng d2 )
by A49, XBOOLE_0:def 4;
then consider t1 being set such that
A51:
( t1 in dom d1 & s = d1 . t1 )
by FUNCT_1:def 5;
consider t2 being set such that
A52:
( t2 in dom d2 & s = d2 . t2 )
by A50, FUNCT_1:def 5;
reconsider W = B ` as non empty Subset of (TOP-REAL 2) by Th19;
A53:
the carrier of ((TOP-REAL 2) | W) <> {}
;
h . (f . t1) = d1 . t1
by A51, FUNCT_1:22;
then A54:
h . (f . t1) = h . (g . t2)
by A51, A52, FUNCT_1:22;
A55:
dom h = the carrier of ((TOP-REAL 2) | (B ` ))
by A53, FUNCT_2:def 1;
A56:
f . t1 in rng f
by A3, A51, FUNCT_1:12;
dom g = the carrier of I[01]
by FUNCT_2:def 1;
then A57:
g . t2 in rng g
by A52, FUNCT_1:12;
then
f . t1 = g . t2
by A2, A12, A19, A54, A55, A56, FUNCT_1:def 8;
then
(rng f) /\ (rng g) <> {}
by A56, A57, XBOOLE_0:def 4;
hence
rng f meets rng g
by XBOOLE_0:def 7; :: thesis: verum