let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & 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); :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & 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); :: thesis: ( 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g )
assume that
A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A2: LE p1,p2,P and
A3: LE p2,p3,P and
A4: LE p3,p4,P ; :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & 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); :: thesis: ( f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 implies rng f meets rng g )
assume that
A5: ( f is continuous & f is one-to-one ) and
A6: ( g is continuous & g is one-to-one ) and
A7: C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } and
A8: f . 0 = p3 and
A9: f . 1 = p1 and
A10: g . 0 = p2 and
A11: g . 1 = p4 and
A12: rng f c= C0 and
A13: rng g c= C0 ; :: thesis: rng f meets rng g
A14: dom f = the carrier of I[01] by FUNCT_2:def 1;
A15: dom g = 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 A16: ( not p1 <> p2 or not p2 <> p3 or not p3 <> p4 ) ; :: thesis: rng f meets rng g
now :: thesis: ( ( p1 = p2 & rng f meets rng g ) or ( p2 = p3 & rng f meets rng g ) or ( p3 = p4 & rng f meets rng g ) )
end;
hence rng f meets rng g ; :: thesis: verum
end;
suppose ( p1 <> p2 & p2 <> p3 & p3 <> p4 ) ; :: thesis: rng f meets rng g
then consider h being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A23: h is being_homeomorphism and
A24: for q being Point of (TOP-REAL 2) holds |.(h . q).| = |.q.| and
A25: |[(- 1),0]| = h . p1 and
A26: |[0,1]| = h . p2 and
A27: |[1,0]| = h . p3 and
A28: |[0,(- 1)]| = h . p4 by A1, A2, A3, A4, JGRAPH_5:67;
A29: h is one-to-one by A23, TOPS_2:def 5;
reconsider f2 = h * f as Function of I[01],(TOP-REAL 2) ;
reconsider g2 = h * g as Function of I[01],(TOP-REAL 2) ;
A30: dom f2 = the carrier of I[01] by FUNCT_2:def 1;
A31: dom g2 = the carrier of I[01] by FUNCT_2:def 1;
A32: f2 . 1 = |[(- 1),0]| by A9, A25, A30, Lm14, BORSUK_1:40, FUNCT_1:12;
A33: g2 . 1 = |[0,(- 1)]| by A11, A28, A31, Lm14, BORSUK_1:40, FUNCT_1:12;
A34: f2 . 0 = |[1,0]| by A8, A27, A30, Lm13, BORSUK_1:40, FUNCT_1:12;
A35: g2 . 0 = |[0,1]| by A10, A26, A31, Lm13, BORSUK_1:40, FUNCT_1:12;
A36: ( f2 is continuous & f2 is one-to-one ) by A5, A23, JGRAPH_5:5, JGRAPH_5:6;
A37: ( g2 is continuous & g2 is one-to-one ) by A6, A23, JGRAPH_5:5, JGRAPH_5:6;
A38: rng f2 c= C0
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f2 or y in C0 )
assume y in rng f2 ; :: thesis: y in C0
then consider x being object such that
A39: x in dom f2 and
A40: y = f2 . x by FUNCT_1:def 3;
A41: f2 . x = h . (f . x) by A39, FUNCT_1:12;
A42: f . x in rng f by A14, A39, FUNCT_1:def 3;
then A43: f . x in C0 by A12;
reconsider qf = f . x as Point of (TOP-REAL 2) by A42;
A44: ex q5 being Point of (TOP-REAL 2) st
( q5 = f . x & |.q5.| <= 1 ) by A7, A43;
|.(h . qf).| = |.qf.| by A24;
hence y in C0 by A7, A40, A41, A44; :: thesis: verum
end;
A45: rng g2 c= C0
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g2 or y in C0 )
assume y in rng g2 ; :: thesis: y in C0
then consider x being object such that
A46: x in dom g2 and
A47: y = g2 . x by FUNCT_1:def 3;
A48: g2 . x = h . (g . x) by A46, FUNCT_1:12;
A49: g . x in rng g by A15, A46, FUNCT_1:def 3;
then A50: g . x in C0 by A13;
reconsider qg = g . x as Point of (TOP-REAL 2) by A49;
A51: ex q5 being Point of (TOP-REAL 2) st
( q5 = g . x & |.q5.| <= 1 ) by A7, A50;
|.(h . qg).| = |.qg.| by A24;
hence y in C0 by A7, A47, A48, A51; :: thesis: verum
end;
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) );
{ 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) ;
reconsider O = 0 , I = 1 as Point of I[01] by BORSUK_1:40, XXREAL_1:1;
- (|[(- 1),0]| `1) = 1 by Lm4;
then A52: f2 . I in KXN by A32, Lm5, Lm12;
A53: f2 . O in KXP by A34, Lm6, Lm7, Lm12;
- (|[0,(- 1)]| `1) = 0 by Lm8;
then A54: g2 . I in KYN by A33, Lm9, Lm12;
- (|[0,1]| `1) = 0 by Lm10;
then g2 . O in KYP by A35, Lm11, Lm12;
then rng f2 meets rng g2 by A7, A36, A37, A38, A45, A52, A53, A54, Th14;
then consider x2 being object such that
A55: x2 in rng f2 and
A56: x2 in rng g2 by XBOOLE_0:3;
consider z2 being object such that
A57: z2 in dom f2 and
A58: x2 = f2 . z2 by A55, FUNCT_1:def 3;
consider z3 being object such that
A59: z3 in dom g2 and
A60: x2 = g2 . z3 by A56, FUNCT_1:def 3;
A61: dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A62: g . z3 in rng g by A15, A59, FUNCT_1:def 3;
A63: f . z2 in rng f by A14, A57, FUNCT_1:def 3;
reconsider h1 = h as Function ;
A64: (h1 ") . x2 = (h1 ") . (h . (f . z2)) by A57, A58, FUNCT_1:12
.= f . z2 by A29, A61, A63, FUNCT_1:34 ;
A65: (h1 ") . x2 = (h1 ") . (h . (g . z3)) by A59, A60, FUNCT_1:12
.= g . z3 by A29, A61, A62, FUNCT_1:34 ;
A66: (h1 ") . x2 in rng f by A14, A57, A64, FUNCT_1:def 3;
(h1 ") . x2 in rng g by A15, A59, A65, FUNCT_1:def 3;
hence rng f meets rng g by A66, XBOOLE_0:3; :: thesis: verum
end;
end;