reconsider O = 0 , I = 1 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
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 = a & p2 `1 = b & p3 `1 = b & p4 `1 = b & c <= p1 `2 & p1 `2 <= d & c <= p4 `2 & p4 `2 < p3 `2 & p3 `2 < p2 `2 & p2 `2 <= d & 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 = a & p2 `1 = b & p3 `1 = b & p4 `1 = b & c <= p1 `2 & p1 `2 <= d & c <= p4 `2 & p4 `2 < p3 `2 & p3 `2 < p2 `2 & p2 `2 <= d & 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 = a & p2 `1 = b & p3 `1 = b & p4 `1 = b & c <= p1 `2 & p1 `2 <= d & c <= p4 `2 & p4 `2 < p3 `2 & p3 `2 < p2 `2 & p2 `2 <= d & 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 that
A1: a < b and
A2: c < d and
A3: p1 `1 = a and
A4: p2 `1 = b and
A5: p3 `1 = b and
A6: p4 `1 = b and
A7: c <= p1 `2 and
A8: p1 `2 <= d and
A9: c <= p4 `2 and
A10: p4 `2 < p3 `2 and
A11: p3 `2 < p2 `2 and
A12: p2 `2 <= d and
A13: f . 0 = p1 and
A14: f . 1 = p3 and
A15: g . 0 = p2 and
A16: g . 1 = p4 and
A17: ( f is continuous & f is one-to-one ) and
A18: ( g is continuous & g is one-to-one ) and
A19: rng f c= closed_inside_of_rectangle a,b,c,d and
A20: 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));
set h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)));
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) ;
A21: p2 `2 > p4 `2 by A10, A11, XXREAL_0:2;
(g . O) `1 = b by A4, A15;
then A22: (g2 . I) `2 >= - 1 by A2, A9, A12, A15, A16, A21, Th65;
d - c > 0 by A2, XREAL_1:52;
then A23: 2 / (d - c) > 0 by XREAL_1:141;
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) ;
A24: (f2 . O) `2 <= 1 by A2, A7, A8, A13, Th60;
A25: (f2 . O) `1 = - 1 by A1, A3, A13, Th54;
A26: ( f2 is continuous & f2 is one-to-one ) by A1, A2, A17, Th53;
A27: rng f2 c= closed_inside_of_rectangle (- 1),1,(- 1),1 by A1, A2, A19, Th52;
A28: (f2 . I) `1 = 1 by A1, A5, A14, Th56;
consider x being Element of (rng f2) /\ (rng g2);
A29: dom f = the carrier of I[01] by FUNCT_2:def 1;
then A30: (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p3 = f2 . I by A14, FUNCT_1:23;
(g . I) `1 = b by A6, A16;
then A31: 1 >= (g2 . O) `2 by A2, A9, A12, A15, A16, A21, Th65;
A32: (g2 . O) `1 = 1 by A1, A4, A15, Th56;
A33: ( g2 is continuous & g2 is one-to-one ) by A1, A2, A18, Th53;
A34: rng g2 c= closed_inside_of_rectangle (- 1),1,(- 1),1 by A1, A2, A20, Th52;
A35: (g2 . I) `1 = 1 by A1, A6, A16, Th56;
b - a > 0 by A1, XREAL_1:52;
then A36: 2 / (b - a) > 0 by XREAL_1:141;
then AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) is being_homeomorphism by A23, Th50;
then A37: AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) is one-to-one by TOPS_2:def 5;
A38: dom g = the carrier of I[01] by FUNCT_2:def 1;
then (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p2 = g2 . O by A15, FUNCT_1:23;
then A39: (g2 . O) `2 > (f2 . I) `2 by A11, A36, A23, A30, Th51;
(AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . p4 = g2 . I by A16, A38, FUNCT_1:23;
then A40: (g2 . I) `2 < (f2 . I) `2 by A10, A36, A23, A30, Th51;
- 1 <= (f2 . O) `2 by A2, A7, A8, A13, Th60;
then rng f2 meets rng g2 by A26, A25, A28, A24, A27, A33, A32, A35, A31, A22, A34, A39, A40, Th30, JGRAPH_6:89;
then A41: (rng f2) /\ (rng g2) <> {} by XBOOLE_0:def 7;
then x in rng g2 by XBOOLE_0:def 4;
then consider z2 being set such that
A42: z2 in dom g2 and
A43: x = g2 . z2 by FUNCT_1:def 5;
A44: x = (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . (g . z2) by A38, A42, A43, FUNCT_1:23;
A45: g . z2 in rng g by A38, A42, FUNCT_1:def 5;
g . z2 in the carrier of (TOP-REAL 2) by A42, FUNCT_2:7;
then A46: g . z2 in dom (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) by FUNCT_2:def 1;
x in rng f2 by A41, XBOOLE_0:def 4;
then consider z1 being set such that
A47: z1 in dom f2 and
A48: x = f2 . z1 by FUNCT_1:def 5;
A49: f . z1 in rng f by A29, A47, FUNCT_1:def 5;
f . z1 in the carrier of (TOP-REAL 2) by A47, FUNCT_2:7;
then A50: f . z1 in dom (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) by FUNCT_2:def 1;
x = (AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) . (f . z1) by A29, A47, A48, FUNCT_1:23;
then f . z1 = g . z2 by A44, A50, A46, A37, FUNCT_1:def 8;
hence rng f meets rng g by A49, A45, XBOOLE_0:3; :: thesis: verum