let p1, p2, p3, p4 be Point of (); :: thesis: for P being non empty compact Subset of ()
for C0 being Subset of () st P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

let P be non empty compact Subset of (); :: thesis: for C0 being Subset of () st P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

let C0 be Subset of (); :: thesis: ( P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P implies for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g )

assume that
A1: P = { p where p is Point of () : |.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],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

let f, g be Function of I[01],(); :: thesis: ( f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p4 & g . 1 = p2 & 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 () : |.p8.| <= 1 } and
A8: f . 0 = p3 and
A9: f . 1 = p1 and
A10: g . 0 = p4 and
A11: g . 1 = p2 and
A12: rng f c= C0 and
A13: rng g c= C0 ; :: thesis:
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:
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 ) )
per cases ( p1 = p2 or p2 = p3 or p3 = p4 ) by A16;
case A17: p1 = p2 ; :: thesis:
A18: p1 in rng f by ;
p2 in rng g by ;
hence rng f meets rng g by ; :: thesis: verum
end;
case A19: p2 = p3 ; :: thesis:
A20: p3 in rng f by ;
p2 in rng g by ;
hence rng f meets rng g by ; :: thesis: verum
end;
case A21: p3 = p4 ; :: thesis:
A22: p3 in rng f by ;
p4 in rng g by ;
hence rng f meets rng g by ; :: thesis: verum
end;
end;
end;
hence rng f meets rng g ; :: thesis: verum
end;
suppose ( p1 <> p2 & p2 <> p3 & p3 <> p4 ) ; :: thesis:
then consider h being Function of (),() such that
A23: h is being_homeomorphism and
A24: for q being Point of () 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 ;
A29: h is one-to-one by ;
reconsider f2 = h * f as Function of I[01],() ;
reconsider g2 = h * g as Function of I[01],() ;
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 ;
A33: g2 . 1 = |[0,1]| by ;
A34: f2 . 0 = |[1,0]| by ;
A35: g2 . 0 = |[0,(- 1)]| by ;
A36: ( f2 is continuous & f2 is one-to-one ) by ;
A37: ( g2 is continuous & g2 is one-to-one ) by ;
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 ;
A42: f . x in rng f by ;
then A43: f . x in C0 by A12;
reconsider qf = f . x as Point of () by A42;
A44: ex q5 being Point of () st
( q5 = f . x & |.q5.| <= 1 ) by ;
|.(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 ;
A49: g . x in rng g by ;
then A50: g . x in C0 by A13;
reconsider qg = g . x as Point of () by A49;
A51: ex q5 being Point of () st
( q5 = g . x & |.q5.| <= 1 ) by ;
|.(h . qg).| = |.qg.| by A24;
hence y in C0 by A7, A47, A48, A51; :: thesis: verum
end;
defpred S1[ Point of ()] means ( |.\$1.| = 1 & \$1 `2 <= \$1 `1 & \$1 `2 >= - (\$1 `1) );
{ q1 where q1 is Point of () : S1[q1] } is Subset of () from then reconsider KXP = { q1 where q1 is Point of () : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } as Subset of () ;
defpred S2[ Point of ()] means ( |.\$1.| = 1 & \$1 `2 >= \$1 `1 & \$1 `2 <= - (\$1 `1) );
{ q2 where q2 is Point of () : S2[q2] } is Subset of () from then reconsider KXN = { q2 where q2 is Point of () : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } as Subset of () ;
defpred S3[ Point of ()] means ( |.\$1.| = 1 & \$1 `2 >= \$1 `1 & \$1 `2 >= - (\$1 `1) );
{ q3 where q3 is Point of () : S3[q3] } is Subset of () from then reconsider KYP = { q3 where q3 is Point of () : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } as Subset of () ;
defpred S4[ Point of ()] means ( |.\$1.| = 1 & \$1 `2 <= \$1 `1 & \$1 `2 <= - (\$1 `1) );
{ q4 where q4 is Point of () : S4[q4] } is Subset of () from then reconsider KYN = { q4 where q4 is Point of () : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } as Subset of () ;
reconsider O = 0 , I = 1 as Point of I[01] by ;
- (|[(- 1),0]| `1) = 1 by Lm4;
then A52: f2 . I in KXN by ;
A53: f2 . O in KXP by ;
- (|[0,(- 1)]| `1) = 0 by Lm8;
then A54: g2 . I in KYP by ;
- (|[0,1]| `1) = 0 by Lm10;
then g2 . O in KYN by ;
then rng f2 meets rng g2 by A7, A36, A37, A38, A45, A52, A53, A54, Th15;
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 ;
consider z3 being object such that
A59: z3 in dom g2 and
A60: x2 = g2 . z3 by ;
A61: dom h = the carrier of () by FUNCT_2:def 1;
A62: g . z3 in rng g by ;
A63: f . z2 in rng f by ;
reconsider h1 = h as Function ;
A64: (h1 ") . x2 = (h1 ") . (h . (f . z2)) by
.= f . z2 by ;
A65: (h1 ") . x2 = (h1 ") . (h . (g . z3)) by
.= g . z3 by ;
A66: (h1 ") . x2 in rng f by ;
(h1 ") . x2 in rng g by ;
hence rng f meets rng g by ; :: thesis: verum
end;
end;