let f, g be Function of I[01] ,(TOP-REAL 2); :: thesis: for a, b, c, d being real number
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & (f . O) `1 = a & (f . I) `1 = b & c <= (f . O) `2 & (f . O) `2 <= d & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & (g . I) `2 = d & a <= (g . O) `1 & (g . O) `1 <= b & a <= (g . I) `1 & (g . I) `1 <= b & a < b & c < d & ( for r being Point of I[01] holds
( not a < (f . r) `1 or not (f . r) `1 < b or not c < (f . r) `2 or not (f . r) `2 < d ) ) & ( for r being Point of I[01] holds
( not a < (g . r) `1 or not (g . r) `1 < b or not c < (g . r) `2 or not (g . r) `2 < d ) ) holds
rng f meets rng g
let a, b, c, d be real number ; :: thesis: for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & (f . O) `1 = a & (f . I) `1 = b & c <= (f . O) `2 & (f . O) `2 <= d & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & (g . I) `2 = d & a <= (g . O) `1 & (g . O) `1 <= b & a <= (g . I) `1 & (g . I) `1 <= b & a < b & c < d & ( for r being Point of I[01] holds
( not a < (f . r) `1 or not (f . r) `1 < b or not c < (f . r) `2 or not (f . r) `2 < d ) ) & ( for r being Point of I[01] holds
( not a < (g . r) `1 or not (g . r) `1 < b or not c < (g . r) `2 or not (g . r) `2 < d ) ) holds
rng f meets rng g
let O, I be Point of I[01] ; :: thesis: ( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & (f . O) `1 = a & (f . I) `1 = b & c <= (f . O) `2 & (f . O) `2 <= d & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & (g . I) `2 = d & a <= (g . O) `1 & (g . O) `1 <= b & a <= (g . I) `1 & (g . I) `1 <= b & a < b & c < d & ( for r being Point of I[01] holds
( not a < (f . r) `1 or not (f . r) `1 < b or not c < (f . r) `2 or not (f . r) `2 < d ) ) & ( for r being Point of I[01] holds
( not a < (g . r) `1 or not (g . r) `1 < b or not c < (g . r) `2 or not (g . r) `2 < d ) ) implies rng f meets rng g )
assume A1: ( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & (f . O) `1 = a & (f . I) `1 = b & c <= (f . O) `2 & (f . O) `2 <= d & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & (g . I) `2 = d & a <= (g . O) `1 & (g . O) `1 <= b & a <= (g . I) `1 & (g . I) `1 <= b & a < b & c < d & ( for r being Point of I[01] holds
( not a < (f . r) `1 or not (f . r) `1 < b or not c < (f . r) `2 or not (f . r) `2 < d ) ) & ( for r being Point of I[01] holds
( not a < (g . r) `1 or not (g . r) `1 < b or not c < (g . r) `2 or not (g . r) `2 < d ) ) ) ; :: thesis: rng f meets rng g
then A2: b - a > 0 by XREAL_1:52;
A3: d - c > 0 by A1, XREAL_1:52;
set A = 2 / (b - a);
set B = 1 - ((2 * b) / (b - a));
set C = 2 / (d - c);
set D = 1 - ((2 * d) / (d - c));
A4: 2 / (b - a) > 0 by A2, XREAL_1:141;
A5: 2 / (d - c) > 0 by A3, XREAL_1:141;
set ff = AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)));
A6: dom (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A7: dom f = the carrier of I[01] by FUNCT_2:def 1;
A8: dom g = the carrier of I[01] by FUNCT_2:def 1;
A9: AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))) is one-to-one by A4, A5, Th54;
reconsider f2 = (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) * f, g2 = (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) * g as Function of I[01] ,(TOP-REAL 2) ;
A12: f2 is one-to-one by A1, A9, FUNCT_1:46;
A13: g2 is one-to-one by A1, A9, FUNCT_1:46;
defpred S₁[ Point of (TOP-REAL 2)] means ( - 1 < $1 `1 & $1 `1 < 1 & - 1 < $1 `2 & $1 `2 < 1 );
reconsider K0 = { p where p is Point of (TOP-REAL 2) : S₁[p] } as Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
A14: f2 . O = (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . (f . O) by A7, FUNCT_1:23
.= |[(((2 / (b - a)) * a) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * ((f . O) `2 )) + (1 - ((2 * d) / (d - c))))]| by A1, Def2 ;
A15: f2 . I = (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . (f . I) by A7, FUNCT_1:23
.= |[(((2 / (b - a)) * b) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * ((f . I) `2 )) + (1 - ((2 * d) / (d - c))))]| by A1, Def2 ;
A16: g2 . O = (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . (g . O) by A8, FUNCT_1:23
.= |[(((2 / (b - a)) * ((g . O) `1 )) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * c) + (1 - ((2 * d) / (d - c))))]| by A1, Def2 ;
A17: g2 . I = (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . (g . I) by A8, FUNCT_1:23
.= |[(((2 / (b - a)) * ((g . I) `1 )) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * d) + (1 - ((2 * d) / (d - c))))]| by A1, Def2 ;
A18: (f2 . O) `1 = - 1

proof

thus (f2 . O) `1 = ((2 / (b - a)) * a) + (1 - ((2 * b) / (b - a))) by A14, EUCLID:56
.= ((a * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= ((a * 2) / (b - a)) + (((b - a) / (b - a)) - ((2 * b) / (b - a))) by A2, XCMPLX_1:60
.= ((a * 2) / (b - a)) + (((b - a) - (2 * b)) / (b - a))
.= ((a * 2) + ((b - a) - (2 * b))) / (b - a)
.= (- (b - a)) / (b - a)
.= - ((b - a) / (b - a))
.= - 1 by A2, XCMPLX_1:60 ; :: thesis: verum

end;

A19: (f2 . I) `1 = ((2 / (b - a)) * b) + (1 - ((2 * b) / (b - a))) by A15, EUCLID:56
.= ((b * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= 1 ;
A20: (g2 . O) `2 = ((2 / (d - c)) * c) + (1 - ((2 * d) / (d - c))) by A16, EUCLID:56
.= ((c * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= ((c * 2) / (d - c)) + (((d - c) / (d - c)) - ((2 * d) / (d - c))) by A3, XCMPLX_1:60
.= ((c * 2) / (d - c)) + (((d - c) - (2 * d)) / (d - c))
.= ((c * 2) + ((d - c) - (2 * d))) / (d - c)
.= (- (d - c)) / (d - c)
.= - ((d - c) / (d - c))
.= - 1 by A3, XCMPLX_1:60 ;
A21: (g2 . I) `2 = ((2 / (d - c)) * d) + (1 - ((2 * d) / (d - c))) by A17, EUCLID:56
.= ((d * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= 1 ;
A22: ( - 1 <= (f2 . O) `2 & (f2 . O) `2 <= 1 & - 1 <= (f2 . I) `2 & (f2 . I) `2 <= 1 )

proof

reconsider s0 = (f . O) `2 as Real ;
A23: (f2 . O) `2 = (((s0 - d) + (s0 - d)) - (c - d)) / (d - c)

proof

thus (f2 . O) `2 = ((2 / (d - c)) * s0) + (1 - ((2 * d) / (d - c))) by A14, EUCLID:56
.= ((s0 * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= ((s0 * 2) / (d - c)) + (((d - c) / (d - c)) - ((2 * d) / (d - c))) by A3, XCMPLX_1:60
.= ((s0 * 2) / (d - c)) + (((d - c) - (2 * d)) / (d - c))
.= ((s0 * 2) + ((d - c) - (2 * d))) / (d - c)
.= (((s0 - d) + (s0 - d)) - (c - d)) / (d - c) ; :: thesis: verum

end;

c - d <= s0 - d by A1, XREAL_1:11;
then (c - d) + (c - d) <= (s0 - d) + (s0 - d) by XREAL_1:9;
then A24: ((c - d) + (c - d)) - (c - d) <= ((s0 - d) + (s0 - d)) - (c - d) by XREAL_1:11;
A25: (c - d) / (d - c) = (- (d - c)) / (d - c)
.= - ((d - c) / (d - c))
.= - 1 by A3, XCMPLX_1:60 ;
d - d >= s0 - d by A1, XREAL_1:11;
then (0 + (d - d)) - (c - d) >= ((s0 - d) + (s0 - d)) - (c - d) by XREAL_1:11;
then A26: (d - c) / (d - c) >= (((s0 - d) + (s0 - d)) - (c - d)) / (d - c) by A3, XREAL_1:74;
reconsider s1 = (f . I) `2 as Real ;
A27: (f2 . I) `2 = (((s1 - d) + (s1 - d)) - (c - d)) / (d - c)

proof

thus (f2 . I) `2 = ((2 / (d - c)) * s1) + (1 - ((2 * d) / (d - c))) by A15, EUCLID:56
.= ((s1 * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= ((s1 * 2) / (d - c)) + (((d - c) / (d - c)) - ((2 * d) / (d - c))) by A3, XCMPLX_1:60
.= ((s1 * 2) / (d - c)) + (((d - c) - (2 * d)) / (d - c))
.= ((s1 * 2) + ((d - c) - (2 * d))) / (d - c)
.= (((s1 - d) + (s1 - d)) - (c - d)) / (d - c) ; :: thesis: verum

end;

c - d <= s1 - d by A1, XREAL_1:11;
then (c - d) + (c - d) <= (s1 - d) + (s1 - d) by XREAL_1:9;
then A28: ((c - d) + (c - d)) - (c - d) <= ((s1 - d) + (s1 - d)) - (c - d) by XREAL_1:11;
d - d >= s1 - d by A1, XREAL_1:11;
then (0 + (d - d)) - (c - d) >= ((s1 - d) + (s1 - d)) - (c - d) by XREAL_1:11;
then (d - c) / (d - c) >= (((s1 - d) + (s1 - d)) - (c - d)) / (d - c) by A3, XREAL_1:74;
hence ( - 1 <= (f2 . O) `2 & (f2 . O) `2 <= 1 & - 1 <= (f2 . I) `2 & (f2 . I) `2 <= 1 ) by A3, A23, A24, A25, A26, A27, A28, XREAL_1:74; :: thesis: verum

end;

A29: ( - 1 <= (g2 . O) `1 & (g2 . O) `1 <= 1 & - 1 <= (g2 . I) `1 & (g2 . I) `1 <= 1 )

proof

reconsider s0 = (g . O) `1 as Real ;
A30: (g2 . O) `1 = (((s0 - b) + (s0 - b)) - (a - b)) / (b - a)

proof

thus (g2 . O) `1 = ((2 / (b - a)) * s0) + (1 - ((2 * b) / (b - a))) by A16, EUCLID:56
.= ((s0 * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= ((s0 * 2) / (b - a)) + (((b - a) / (b - a)) - ((2 * b) / (b - a))) by A2, XCMPLX_1:60
.= ((s0 * 2) / (b - a)) + (((b - a) - (2 * b)) / (b - a))
.= ((s0 * 2) + ((b - a) - (2 * b))) / (b - a)
.= (((s0 - b) + (s0 - b)) - (a - b)) / (b - a) ; :: thesis: verum

end;

a - b <= s0 - b by A1, XREAL_1:11;
then (a - b) + (a - b) <= (s0 - b) + (s0 - b) by XREAL_1:9;
then A31: ((a - b) + (a - b)) - (a - b) <= ((s0 - b) + (s0 - b)) - (a - b) by XREAL_1:11;
A32: (a - b) / (b - a) = (- (b - a)) / (b - a)
.= - ((b - a) / (b - a))
.= - 1 by A2, XCMPLX_1:60 ;
b - b >= s0 - b by A1, XREAL_1:11;
then (0 + (b - b)) - (a - b) >= ((s0 - b) + (s0 - b)) - (a - b) by XREAL_1:11;
then A33: (b - a) / (b - a) >= (((s0 - b) + (s0 - b)) - (a - b)) / (b - a) by A2, XREAL_1:74;
reconsider s1 = (g . I) `1 as Real ;
A34: (g2 . I) `1 = (((s1 - b) + (s1 - b)) - (a - b)) / (b - a)

proof

thus (g2 . I) `1 = ((2 / (b - a)) * s1) + (1 - ((2 * b) / (b - a))) by A17, EUCLID:56
.= ((s1 * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= ((s1 * 2) / (b - a)) + (((b - a) / (b - a)) - ((2 * b) / (b - a))) by A2, XCMPLX_1:60
.= ((s1 * 2) / (b - a)) + (((b - a) - (2 * b)) / (b - a))
.= ((s1 * 2) + ((b - a) - (2 * b))) / (b - a)
.= (((s1 - b) + (s1 - b)) - (a - b)) / (b - a) ; :: thesis: verum

end;

a - b <= s1 - b by A1, XREAL_1:11;
then (a - b) + (a - b) <= (s1 - b) + (s1 - b) by XREAL_1:9;
then A35: ((a - b) + (a - b)) - (a - b) <= ((s1 - b) + (s1 - b)) - (a - b) by XREAL_1:11;
b - b >= s1 - b by A1, XREAL_1:11;
then (0 + (b - b)) - (a - b) >= ((s1 - b) + (s1 - b)) - (a - b) by XREAL_1:11;
then (b - a) / (b - a) >= (((s1 - b) + (s1 - b)) - (a - b)) / (b - a) by A2, XREAL_1:74;
hence ( - 1 <= (g2 . O) `1 & (g2 . O) `1 <= 1 & - 1 <= (g2 . I) `1 & (g2 . I) `1 <= 1 ) by A2, A30, A31, A32, A33, A34, A35, XREAL_1:74; :: thesis: verum

end;

A36: now

assume rng f2 meets K0 ; :: thesis: contradiction
then consider x being set such that
A37: ( x in rng f2 & x in K0 ) by XBOOLE_0:3;
reconsider q = x as Point of (TOP-REAL 2) by A37;
consider p being Point of (TOP-REAL 2) such that
A38: ( p = q & - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) by A37;
consider z being set such that
A39: ( z in dom f2 & x = f2 . z ) by A37, FUNCT_1:def 5;
reconsider u = z as Point of I[01] by A39;
reconsider t = f . u as Point of (TOP-REAL 2) ;
A40: (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . t = |[(((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * (t `2 )) + (1 - ((2 * d) / (d - c))))]| by Def2;
(AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . t = p by A38, A39, FUNCT_1:22;
then A41: ( - 1 < ((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a))) & ((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a))) < 1 & - 1 < ((2 / (d - c)) * (t `2 )) + (1 - ((2 * d) / (d - c))) & ((2 / (d - c)) * (t `2 )) + (1 - ((2 * d) / (d - c))) < 1 ) by A38, A40, EUCLID:56;
A42: ((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a))) = ((2 * ((t `1 ) - b)) - (a - b)) / (b - a)

proof

thus ((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a))) = (((t `1 ) * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= (((t `1 ) * 2) / (b - a)) + (((b - a) / (b - a)) - ((2 * b) / (b - a))) by A2, XCMPLX_1:60
.= (((t `1 ) * 2) / (b - a)) + (((b - a) - (2 * b)) / (b - a))
.= (((t `1 ) * 2) + ((b - a) - (2 * b))) / (b - a)
.= ((2 * ((t `1 ) - b)) - (a - b)) / (b - a) ; :: thesis: verum

end;

then (- 1) * (b - a) < (((2 * ((t `1 ) - b)) - (a - b)) / (b - a)) * (b - a) by A2, A41, XREAL_1:70;
then (- 1) * (b - a) < (2 * ((t `1 ) - b)) - (a - b) by A2, XCMPLX_1:88;
then ((- 1) * (b - a)) + (a - b) < ((2 * ((t `1 ) - b)) - (a - b)) + (a - b) by XREAL_1:10;
then (2 * (a - b)) / 2 < (2 * ((t `1 ) - b)) / 2 by XREAL_1:76;
then A43: a < t `1 by XREAL_1:11;
1 * (b - a) > (((2 * ((t `1 ) - b)) - (a - b)) / (b - a)) * (b - a) by A2, A41, A42, XREAL_1:70;
then 1 * (b - a) > (2 * ((t `1 ) - b)) - (a - b) by A2, XCMPLX_1:88;
then (1 * (b - a)) + (a - b) > ((2 * ((t `1 ) - b)) - (a - b)) + (a - b) by XREAL_1:10;
then 0 / 2 > (((t `1 ) - b) * 2) / 2 ;
then A44: 0 + b > t `1 by XREAL_1:21;
A45: ((2 / (d - c)) * (t `2 )) + (1 - ((2 * d) / (d - c))) = (((t `2 ) * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= (((t `2 ) * 2) / (d - c)) + (((d - c) / (d - c)) - ((2 * d) / (d - c))) by A3, XCMPLX_1:60
.= (((t `2 ) * 2) / (d - c)) + (((d - c) - (2 * d)) / (d - c))
.= (((t `2 ) * 2) + ((d - c) - (2 * d))) / (d - c)
.= ((2 * ((t `2 ) - d)) - (c - d)) / (d - c) ;
then (- 1) * (d - c) < (((2 * ((t `2 ) - d)) - (c - d)) / (d - c)) * (d - c) by A3, A41, XREAL_1:70;
then (- 1) * (d - c) < (2 * ((t `2 ) - d)) - (c - d) by A3, XCMPLX_1:88;
then ((- 1) * (d - c)) + (c - d) < ((2 * ((t `2 ) - d)) - (c - d)) + (c - d) by XREAL_1:10;
then (2 * (c - d)) / 2 < (2 * ((t `2 ) - d)) / 2 by XREAL_1:76;
then A46: c < t `2 by XREAL_1:11;
1 * (d - c) > (((2 * ((t `2 ) - d)) - (c - d)) / (d - c)) * (d - c) by A3, A41, A45, XREAL_1:70;
then 1 * (d - c) > (2 * ((t `2 ) - d)) - (c - d) by A3, XCMPLX_1:88;
then (1 * (d - c)) + (c - d) > ((2 * ((t `2 ) - d)) - (c - d)) + (c - d) by XREAL_1:10;
then 0 / 2 > (((t `2 ) - d) * 2) / 2 ;
then 0 + d > t `2 by XREAL_1:21;
hence contradiction by A1, A43, A44, A46; :: thesis: verum

end;

now

assume rng g2 meets K0 ; :: thesis: contradiction
then consider x being set such that
A47: ( x in rng g2 & x in K0 ) by XBOOLE_0:3;
reconsider q = x as Point of (TOP-REAL 2) by A47;
consider p being Point of (TOP-REAL 2) such that
A48: ( p = q & - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) by A47;
consider z being set such that
A49: ( z in dom g2 & x = g2 . z ) by A47, FUNCT_1:def 5;
reconsider u = z as Point of I[01] by A49;
reconsider t = g . u as Point of (TOP-REAL 2) ;
A50: (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . t = |[(((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * (t `2 )) + (1 - ((2 * d) / (d - c))))]| by Def2;
(AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . t = p by A48, A49, FUNCT_1:22;
then A51: ( - 1 < ((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a))) & ((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a))) < 1 & - 1 < ((2 / (d - c)) * (t `2 )) + (1 - ((2 * d) / (d - c))) & ((2 / (d - c)) * (t `2 )) + (1 - ((2 * d) / (d - c))) < 1 ) by A48, A50, EUCLID:56;
A52: ((2 / (b - a)) * (t `1 )) + (1 - ((2 * b) / (b - a))) = (((t `1 ) * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= (((t `1 ) * 2) / (b - a)) + (((b - a) / (b - a)) - ((2 * b) / (b - a))) by A2, XCMPLX_1:60
.= (((t `1 ) * 2) / (b - a)) + (((b - a) - (2 * b)) / (b - a))
.= (((t `1 ) * 2) + ((b - a) - (2 * b))) / (b - a)
.= ((2 * ((t `1 ) - b)) - (a - b)) / (b - a) ;
then (- 1) * (b - a) < (((2 * ((t `1 ) - b)) - (a - b)) / (b - a)) * (b - a) by A2, A51, XREAL_1:70;
then (- 1) * (b - a) < (2 * ((t `1 ) - b)) - (a - b) by A2, XCMPLX_1:88;
then ((- 1) * (b - a)) + (a - b) < ((2 * ((t `1 ) - b)) - (a - b)) + (a - b) by XREAL_1:10;
then (2 * (a - b)) / 2 < (2 * ((t `1 ) - b)) / 2 by XREAL_1:76;
then A53: a < t `1 by XREAL_1:11;
1 * (b - a) > (((2 * ((t `1 ) - b)) - (a - b)) / (b - a)) * (b - a) by A2, A51, A52, XREAL_1:70;
then 1 * (b - a) > (2 * ((t `1 ) - b)) - (a - b) by A2, XCMPLX_1:88;
then (1 * (b - a)) + (a - b) > ((2 * ((t `1 ) - b)) - (a - b)) + (a - b) by XREAL_1:10;
then 0 / 2 > (((t `1 ) - b) * 2) / 2 ;
then A54: 0 + b > t `1 by XREAL_1:21;
A55: ((2 / (d - c)) * (t `2 )) + (1 - ((2 * d) / (d - c))) = (((t `2 ) * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= (((t `2 ) * 2) / (d - c)) + (((d - c) / (d - c)) - ((2 * d) / (d - c))) by A3, XCMPLX_1:60
.= (((t `2 ) * 2) / (d - c)) + (((d - c) - (2 * d)) / (d - c))
.= (((t `2 ) * 2) + ((d - c) - (2 * d))) / (d - c)
.= ((2 * ((t `2 ) - d)) - (c - d)) / (d - c) ;
then (- 1) * (d - c) < (((2 * ((t `2 ) - d)) - (c - d)) / (d - c)) * (d - c) by A3, A51, XREAL_1:70;
then (- 1) * (d - c) < (2 * ((t `2 ) - d)) - (c - d) by A3, XCMPLX_1:88;
then ((- 1) * (d - c)) + (c - d) < ((2 * ((t `2 ) - d)) - (c - d)) + (c - d) by XREAL_1:10;
then (2 * (c - d)) / 2 < (2 * ((t `2 ) - d)) / 2 by XREAL_1:76;
then A56: c < t `2 by XREAL_1:11;
1 * (d - c) > (((2 * ((t `2 ) - d)) - (c - d)) / (d - c)) * (d - c) by A3, A51, A55, XREAL_1:70;
then 1 * (d - c) > (2 * ((t `2 ) - d)) - (c - d) by A3, XCMPLX_1:88;
then (1 * (d - c)) + (c - d) > ((2 * ((t `2 ) - d)) - (c - d)) + (c - d) by XREAL_1:10;
then 0 / 2 > (((t `2 ) - d) * 2) / 2 ;
then 0 + d > t `2 by XREAL_1:21;
hence contradiction by A1, A53, A54, A56; :: thesis: verum

end;

then rng f2 meets rng g2 by A1, A12, A13, A18, A19, A20, A21, A22, A29, A36, Th52;
then A57: (rng f2) /\ (rng g2) <> {} by XBOOLE_0:def 7;
consider y being Element of (rng f2) /\ (rng g2);
A58: ( y in rng f2 & y in rng g2 ) by A57, XBOOLE_0:def 4;
then consider x being set such that
A59: ( x in dom f2 & y = f2 . x ) by FUNCT_1:def 5;
A60: y = (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . (f . x) by A59, FUNCT_1:22;
consider x2 being set such that
A61: ( x2 in dom g2 & y = g2 . x2 ) by A58, FUNCT_1:def 5;
A62: y = (AffineMap (2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) . (g . x2) by A61, FUNCT_1:22;
dom f2 c= dom f by RELAT_1:44;
then A63: f . x in rng f by A59, FUNCT_1:12;
dom g2 c= dom g by RELAT_1:44;
then A64: g . x2 in rng g by A61, FUNCT_1:12;
then f . x = g . x2 by A6, A9, A60, A62, A63, FUNCT_1:def 8;
then (rng f) /\ (rng g) <> {} by A63, A64, XBOOLE_0:def 4;
hence rng f meets rng g by XBOOLE_0:def 7; :: thesis: verum