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