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