let p1, p2, p3, p4 be Point of (TOP-REAL 2); for P being non empty compact Subset of (TOP-REAL 2)
for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],(TOP-REAL 2) st 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 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let P be non empty compact Subset of (TOP-REAL 2); for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],(TOP-REAL 2) st 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 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let C0 be Subset of (TOP-REAL 2); ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P implies for f, g being Function of I[01],(TOP-REAL 2) st 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 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g )
assume A1:
( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P )
; for f, g being Function of I[01],(TOP-REAL 2) st 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 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let f, g be Function of I[01],(TOP-REAL 2); ( 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 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 implies rng f meets rng g )
assume A2:
( 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 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 )
; rng f meets rng g
A3:
dom g = the carrier of I[01]
by FUNCT_2:def 1;
A4:
dom f = the carrier of I[01]
by FUNCT_2:def 1;
per cases
( not p1 <> p2 or not p2 <> p3 or not p3 <> p4 or ( p1 <> p2 & p2 <> p3 & p3 <> p4 ) )
;
suppose
(
p1 <> p2 &
p2 <> p3 &
p3 <> p4 )
;
rng f meets rng gthen consider h being
Function of
(TOP-REAL 2),
(TOP-REAL 2) such that A9:
h is
being_homeomorphism
and A10:
for
q being
Point of
(TOP-REAL 2) holds
|.(h . q).| = |.q.|
and A11:
|[(- 1),0]| = h . p1
and A12:
|[0,1]| = h . p2
and A13:
|[1,0]| = h . p3
and A14:
|[0,(- 1)]| = h . p4
by A1, Th67;
reconsider f2 =
h * f,
g2 =
h * g as
Function of
I[01],
(TOP-REAL 2) ;
A15:
- (|[0,(- 1)]| `1) = 0
by Lm10;
A16:
rng g2 c= C0
A22:
rng f2 c= C0
reconsider h1 =
h as
Function ;
reconsider O =
0 ,
I = 1 as
Point of
I[01] by BORSUK_1:40, XXREAL_1:1;
defpred S1[
Point of
(TOP-REAL 2)]
means (
|.$1.| = 1 & $1
`2 <= $1
`1 & $1
`2 >= - ($1 `1) );
{ q1 where q1 is Point of (TOP-REAL 2) : S1[q1] } is
Subset of
(TOP-REAL 2)
from JGRAPH_2:sch 1();
then reconsider KXP =
{ q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } as
Subset of
(TOP-REAL 2) ;
defpred S2[
Point of
(TOP-REAL 2)]
means (
|.$1.| = 1 & $1
`2 >= $1
`1 & $1
`2 <= - ($1 `1) );
A28:
dom h = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
{ q2 where q2 is Point of (TOP-REAL 2) : S2[q2] } is
Subset of
(TOP-REAL 2)
from JGRAPH_2:sch 1();
then reconsider KXN =
{ q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } as
Subset of
(TOP-REAL 2) ;
defpred S3[
Point of
(TOP-REAL 2)]
means (
|.$1.| = 1 & $1
`2 >= $1
`1 & $1
`2 >= - ($1 `1) );
{ q3 where q3 is Point of (TOP-REAL 2) : S3[q3] } is
Subset of
(TOP-REAL 2)
from JGRAPH_2:sch 1();
then reconsider KYP =
{ q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } as
Subset of
(TOP-REAL 2) ;
defpred S4[
Point of
(TOP-REAL 2)]
means (
|.$1.| = 1 & $1
`2 <= $1
`1 & $1
`2 <= - ($1 `1) );
{ q4 where q4 is Point of (TOP-REAL 2) : S4[q4] } is
Subset of
(TOP-REAL 2)
from JGRAPH_2:sch 1();
then reconsider KYN =
{ q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } as
Subset of
(TOP-REAL 2) ;
A29:
- (|[(- 1),0]| `1) = 1
by Lm7;
A30:
- (|[0,1]| `1) = 0
by Lm12;
A31:
dom g2 = the
carrier of
I[01]
by FUNCT_2:def 1;
then
g2 . 0 = |[0,1]|
by A2, A12, Lm15, BORSUK_1:40, FUNCT_1:12;
then A32:
g2 . O in KYP
by A30, Lm13, Lm14;
g2 . 1
= |[0,(- 1)]|
by A2, A14, A31, Lm16, BORSUK_1:40, FUNCT_1:12;
then A33:
g2 . I in KYN
by A15, Lm11, Lm14;
A34:
dom f2 = the
carrier of
I[01]
by FUNCT_2:def 1;
then
f2 . 1
= |[1,0]|
by A2, A13, Lm16, BORSUK_1:40, FUNCT_1:12;
then A35:
f2 . I in KXP
by Lm9, Lm14;
f2 . 0 = |[(- 1),0]|
by A2, A11, A34, Lm15, BORSUK_1:40, FUNCT_1:12;
then A36:
f2 . O in KXN
by A29, Lm8, Lm14;
A37:
h is
one-to-one
by A9, TOPS_2:def 5;
(
f2 is
continuous &
f2 is
one-to-one &
g2 is
continuous &
g2 is
one-to-one )
by A2, A9, Th5, Th6;
then
rng f2 meets rng g2
by A2, A22, A16, A36, A35, A33, A32, Th15;
then consider x2 being
object such that A38:
x2 in rng f2
and A39:
x2 in rng g2
by XBOOLE_0:3;
consider z3 being
object such that A40:
z3 in dom g2
and A41:
x2 = g2 . z3
by A39, FUNCT_1:def 3;
A42:
g . z3 in rng g
by A3, A40, FUNCT_1:def 3;
(h1 ") . x2 =
(h1 ") . (h . (g . z3))
by A40, A41, FUNCT_1:12
.=
g . z3
by A37, A28, A42, FUNCT_1:34
;
then A43:
(h1 ") . x2 in rng g
by A3, A40, FUNCT_1:def 3;
consider z2 being
object such that A44:
z2 in dom f2
and A45:
x2 = f2 . z2
by A38, FUNCT_1:def 3;
A46:
f . z2 in rng f
by A4, A44, FUNCT_1:def 3;
(h1 ") . x2 =
(h1 ") . (h . (f . z2))
by A44, A45, FUNCT_1:12
.=
f . z2
by A37, A28, A46, FUNCT_1:34
;
then
(h1 ") . x2 in rng f
by A4, A44, FUNCT_1:def 3;
hence
rng f meets rng g
by A43, XBOOLE_0:3;
verum end; end;