let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: ( p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) 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 & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) holds
rng f meets rng g )
set K = rectangle ((- 1),1,(- 1),1);
set K0 = closed_inside_of_rectangle ((- 1),1,(- 1),1);
assume A1: p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) ; :: 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 & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) holds
rng f meets rng g
reconsider j = 1 as non negative Real ;
reconsider P = circle (0,0,j) as non empty compact Subset of (TOP-REAL 2) ;
A2: P = { p6 where p6 is Point of (TOP-REAL 2) : |.p6.| = 1 } by Th24;
thus 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 & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) holds
rng f meets rng g :: thesis: verum
proof
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 & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) implies rng f meets rng g )
assume that
A3: ( f is continuous & f is one-to-one ) and
A4: ( g is continuous & g is one-to-one ) and
A5: f . 0 = p1 and
A6: f . 1 = p3 and
A7: g . 0 = p2 and
A8: g . 1 = p4 and
A9: rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) and
A10: rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) ; :: thesis: rng f meets rng g
reconsider s = Sq_Circ as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A11: dom s = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
reconsider f1 = s * f as Function of I[01],(TOP-REAL 2) ;
reconsider g1 = s * g as Function of I[01],(TOP-REAL 2) ;
s is being_homeomorphism by JGRAPH_3:43;
then A12: s is continuous by TOPS_2:def 5;
A13: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then 0 in dom f by XXREAL_1:1;
then A14: f1 . 0 = Sq_Circ . p1 by A5, FUNCT_1:13;
1 in dom f by A13, XXREAL_1:1;
then A15: f1 . 1 = Sq_Circ . p3 by A6, FUNCT_1:13;
A16: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then 0 in dom g by XXREAL_1:1;
then A17: g1 . 0 = Sq_Circ . p2 by A7, FUNCT_1:13;
1 in dom g by A16, XXREAL_1:1;
then A18: g1 . 1 = Sq_Circ . p4 by A8, FUNCT_1:13;
defpred S1[ Point of (TOP-REAL 2)] means |.$1.| <= 1;
{ p8 where p8 is Point of (TOP-REAL 2) : S1[p8] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
 then reconsider C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } as Subset of (TOP-REAL 2) ;
A19: s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) = C0 by Th27;
A20: rng f1 c= C0
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f1 or y in C0 )
assume y in rng f1 ; :: thesis: y in C0
then consider x being object such that
A21: x in dom f1 and
A22: y = f1 . x by FUNCT_1:def 3;
A23: x in dom f by A21, FUNCT_1:11;
A24: f . x in dom s by A21, FUNCT_1:11;
f . x in rng f by A23, FUNCT_1:3;
then s . (f . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) by A9, A24, FUNCT_1:def 6;
hence y in C0 by A19, A21, A22, FUNCT_1:12; :: thesis: verum
end;
A25: rng g1 c= C0
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g1 or y in C0 )
assume y in rng g1 ; :: thesis: y in C0
then consider x being object such that
A26: x in dom g1 and
A27: y = g1 . x by FUNCT_1:def 3;
A28: x in dom g by A26, FUNCT_1:11;
A29: g . x in dom s by A26, FUNCT_1:11;
g . x in rng g by A28, FUNCT_1:3;
then s . (g . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) by A10, A29, FUNCT_1:def 6;
hence y in C0 by A19, A26, A27, FUNCT_1:12; :: thesis: verum
end;
reconsider q1 = s . p1, q2 = s . p2, q3 = s . p3, q4 = s . p4 as Point of (TOP-REAL 2) ;
q1,q2,q3,q4 are_in_this_order_on P by A1, Th78;
then rng f1 meets rng g1 by A2, A3, A4, A12, A14, A15, A17, A18, A20, A25, Th18;
then consider y being object such that
A30: y in rng f1 and
A31: y in rng g1 by XBOOLE_0:3;
consider x1 being object such that
A32: x1 in dom f1 and
A33: y = f1 . x1 by A30, FUNCT_1:def 3;
consider x2 being object such that
A34: x2 in dom g1 and
A35: y = g1 . x2 by A31, FUNCT_1:def 3;
dom f1 c= dom f by RELAT_1:25;
then A36: f . x1 in rng f by A32, FUNCT_1:3;
dom g1 c= dom g by RELAT_1:25;
then A37: g . x2 in rng g by A34, FUNCT_1:3;
y = Sq_Circ . (f . x1) by A32, A33, FUNCT_1:12;
then A38: (Sq_Circ ") . y = f . x1 by A11, A36, FUNCT_1:32;
x1 in dom f by A32, FUNCT_1:11;
then A39: f . x1 in rng f by FUNCT_1:def 3;
y = Sq_Circ . (g . x2) by A34, A35, FUNCT_1:12;
then A40: (Sq_Circ ") . y = g . x2 by A11, A37, FUNCT_1:32;
x2 in dom g by A34, FUNCT_1:11;
then g . x2 in rng g by FUNCT_1:def 3;
hence rng f meets rng g by A38, A39, A40, XBOOLE_0:3; :: thesis: verum
end;