let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for a, b, c, d being real number
for f, g being Function of I[01] ,(TOP-REAL 2) st a < b & c < d & p1 `1 = b & p2 `1 = b & p3 `1 = b & p4 `1 = b & d >= p1 `2 & p1 `2 > p2 `2 & p2 `2 > p3 `2 & p3 `2 > p4 `2 & p4 `2 >= c & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & rng f c= closed_inside_of_rectangle a,b,c,d & rng g c= closed_inside_of_rectangle a,b,c,d holds
rng f meets rng g
let a, b, c, d be real number ; :: thesis: for f, g being Function of I[01] ,(TOP-REAL 2) st a < b & c < d & p1 `1 = b & p2 `1 = b & p3 `1 = b & p4 `1 = b & d >= p1 `2 & p1 `2 > p2 `2 & p2 `2 > p3 `2 & p3 `2 > p4 `2 & p4 `2 >= c & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & rng f c= closed_inside_of_rectangle a,b,c,d & rng g c= closed_inside_of_rectangle a,b,c,d holds
rng f meets rng g
let f, g be Function of I[01] ,(TOP-REAL 2); :: thesis: ( a < b & c < d & p1 `1 = b & p2 `1 = b & p3 `1 = b & p4 `1 = b & d >= p1 `2 & p1 `2 > p2 `2 & p2 `2 > p3 `2 & p3 `2 > p4 `2 & p4 `2 >= c & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & rng f c= closed_inside_of_rectangle a,b,c,d & rng g c= closed_inside_of_rectangle a,b,c,d implies rng f meets rng g )
assume A1: ( a < b & c < d & p1 `1 = b & p2 `1 = b & p3 `1 = b & p4 `1 = b & d >= p1 `2 & p1 `2 > p2 `2 & p2 `2 > p3 `2 & p3 `2 > p4 `2 & p4 `2 >= c & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & rng f c= closed_inside_of_rectangle a,b,c,d & rng g c= closed_inside_of_rectangle a,b,c,d ) ; :: thesis: rng f meets rng g
set A = 2 / (b - a);
set B = - ((b + a) / (b - a));
set C = 2 / (d - c);
set D = - ((d + c) / (d - c));
b - a > 0 by A1, XREAL_1:52;
then A2: 2 / (b - a) > 0 by XREAL_1:141;
d - c > 0 by A1, XREAL_1:52;
then A3: 2 / (d - c) > 0 by XREAL_1:141;
set h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)));
A4: p1 `2 > p3 `2 by A1, XXREAL_0:2;
A5: p3 `2 > c by A1, XXREAL_0:2;
A6: p2 `2 > p4 `2 by A1, XXREAL_0:2;
A7: d > p2 `2 by A1, XXREAL_0:2;
A8: ( AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) is being_homeomorphism & ( for p11, p21 being Point of (TOP-REAL 2) st p11 `2 < p21 `2 holds
((AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p11) `2 < ((AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p21) `2 ) ) by A2, A3, Th51;
A9: ((AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p1) `2 > ((AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p2) `2 by A1, A2, A3, Th51;
A10: ((AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p2) `2 > ((AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p3) `2 by A1, A2, A3, Th51;
A11: ((AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p3) `2 > ((AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p4) `2 by A1, A2, A3, Th51;
reconsider f2 = (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) * f as Function of I[01] ,(TOP-REAL 2) ;
reconsider g2 = (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) * g as Function of I[01] ,(TOP-REAL 2) ;
reconsider O = 0 , I = 1 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
A12: dom f = the carrier of I[01] by FUNCT_2:def 1;
A13: dom g = the carrier of I[01] by FUNCT_2:def 1;
A14: (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p1 = f2 . O by A1, A12, FUNCT_1:23;
A15: (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p2 = g2 . O by A1, A13, FUNCT_1:23;
A16: (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p3 = f2 . I by A1, A12, FUNCT_1:23;
A17: (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p4 = g2 . I by A1, A13, FUNCT_1:23;
A18: ( (f . O) `1 = b & (f . I) `1 = b ) by A1;
A19: ( f2 is continuous & f2 is one-to-one ) by A1, Th53;
A20: ( (f2 . O) `1 = 1 & (f2 . I) `1 = 1 ) by A1, Th56;
A21: ( 1 >= (f2 . O) `2 & (f2 . O) `2 > (f2 . I) `2 & (f2 . I) `2 >= - 1 ) by A1, A4, A5, A18, Th65;
A22: rng f2 c= closed_inside_of_rectangle (- 1),1,(- 1),1 by A1, Th52;
A23: ( (g . O) `1 = b & (g . I) `1 = b ) by A1;
A24: ( g2 is continuous & g2 is one-to-one ) by A1, Th53;
A25: ( (g2 . O) `1 = 1 & (g2 . I) `1 = 1 ) by A1, Th56;
A26: ( 1 >= (g2 . O) `2 & (g2 . O) `2 > (g2 . I) `2 & (g2 . I) `2 >= - 1 ) by A1, A6, A7, A23, Th65;
X: rng g2 c= closed_inside_of_rectangle (- 1),1,(- 1),1 by A1, Th52;
then f2 . O,g2 . O,f2 . I,g2 . I are_in_this_order_on rectangle (- 1),1,(- 1),1 by A9, A10, A11, A14, A15, A16, A17, A19, A20, A21, A22, A24, A25, A26, Th44;
then rng f2 meets rng g2 by A9, A10, A11, A14, A15, A16, A17, A19, A20, A21, A22, A24, A25, A26, JGRAPH_6:89, X;
then A27: (rng f2) /\ (rng g2) <> {} by XBOOLE_0:def 7;
consider x being Element of (rng f2) /\ (rng g2);
A28: ( x in rng f2 & x in rng g2 ) by A27, XBOOLE_0:def 4;
then consider z1 being set such that
A29: ( z1 in dom f2 & x = f2 . z1 ) by FUNCT_1:def 5;
consider z2 being set such that
A30: ( z2 in dom g2 & x = g2 . z2 ) by A28, FUNCT_1:def 5;
A31: x = (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . (f . z1) by A12, A29, FUNCT_1:23;
A32: x = (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . (g . z2) by A13, A30, FUNCT_1:23;
A33: f . z1 in rng f by A12, A29, FUNCT_1:def 5;
A34: g . z2 in rng g by A13, A30, FUNCT_1:def 5;
f . z1 in the carrier of (TOP-REAL 2) by A29, FUNCT_2:7;
then A35: f . z1 in dom (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) by FUNCT_2:def 1;
g . z2 in the carrier of (TOP-REAL 2) by A30, FUNCT_2:7;
then A36: g . z2 in dom (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) by FUNCT_2:def 1;
AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) is one-to-one by A8, TOPS_2:def 5;
then f . z1 = g . z2 by A31, A32, A35, A36, FUNCT_1:def 8;
hence rng f meets rng g by A33, A34, XBOOLE_0:3; :: thesis: verum