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();
let f, g be Function of I[01],(TOP-REAL 2); :: thesis: for a, b, c, d being Real
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; :: 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 that
A1: ( O = 0 & I = 1 ) and
A2: ( f is continuous & f is one-to-one & g is continuous & g is one-to-one ) and
A3: (f . O) `1 = a and
A4: (f . I) `1 = b and
A5: c <= (f . O) `2 and
A6: (f . O) `2 <= d and
A7: c <= (f . I) `2 and
A8: (f . I) `2 <= d and
A9: (g . O) `2 = c and
A10: (g . I) `2 = d and
A11: a <= (g . O) `1 and
A12: (g . O) `1 <= b and
A13: a <= (g . I) `1 and
A14: (g . I) `1 <= b and
A15: a < b and
A16: c < d and
A17: 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 ) and
A18: 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
set A = 2 / (b - a);
set B = 1 - ((2 * b) / (b - a));
set C = 2 / (d - c);
set D = 1 - ((2 * d) / (d - c));
set ff = AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))));
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) ;
A19: d - c > 0 by A16, XREAL_1:50;
then A20: 2 / (d - c) > 0 by XREAL_1:139;
A21: dom g = the carrier of I[01] by FUNCT_2:def 1;
then A22: g2 . I = (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) . (g . I) by FUNCT_1:13
.= |[(((2 / (b - a)) * ((g . I) `1)) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * d) + (1 - ((2 * d) / (d - c))))]| by A10, Def2 ;
then A23: (g2 . I) `2 = ((2 / (d - c)) * d) + (1 - ((2 * d) / (d - c))) by EUCLID:52
.= ((d * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= 1 ;
A24: g2 . O = (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) . (g . O) by A21, FUNCT_1:13
.= |[(((2 / (b - a)) * ((g . O) `1)) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * c) + (1 - ((2 * d) / (d - c))))]| by A9, Def2 ;
then A25: (g2 . O) `2 = ((2 / (d - c)) * c) + (1 - ((2 * d) / (d - c))) by EUCLID:52
.= ((c * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= ((c * 2) / (d - c)) + (((d - c) / (d - c)) - ((2 * d) / (d - c))) by A19, 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 A19, XCMPLX_1:60 ;
A26: b - a > 0 by A15, XREAL_1:50;
A27: ( - 1 <= (g2 . O) `1 & (g2 . O) `1 <= 1 & - 1 <= (g2 . I) `1 & (g2 . I) `1 <= 1 )

proof

reconsider s1 = (g . I) `1 as Real ;
reconsider s0 = (g . O) `1 as Real ;
A28: (a - b) / (b - a) = (- (b - a)) / (b - a)
.= - ((b - a) / (b - a))
.= - 1 by A26, XCMPLX_1:60 ;
A29: (g2 . I) `1 = ((2 / (b - a)) * s1) + (1 - ((2 * b) / (b - a))) by A22, EUCLID:52
.= ((s1 * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= ((s1 * 2) / (b - a)) + (((b - a) / (b - a)) - ((2 * b) / (b - a))) by A26, 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) ;
b - b >= s0 - b by A12, XREAL_1:9;
then (0 + (b - b)) - (a - b) >= ((s0 - b) + (s0 - b)) - (a - b) by XREAL_1:9;
then A30: (b - a) / (b - a) >= (((s0 - b) + (s0 - b)) - (a - b)) / (b - a) by A26, XREAL_1:72;
b - b >= s1 - b by A14, XREAL_1:9;
then A31: (0 + (b - b)) - (a - b) >= ((s1 - b) + (s1 - b)) - (a - b) by XREAL_1:9;
a - b <= s1 - b by A13, XREAL_1:9;
then (a - b) + (a - b) <= (s1 - b) + (s1 - b) by XREAL_1:7;
then A32: ((a - b) + (a - b)) - (a - b) <= ((s1 - b) + (s1 - b)) - (a - b) by XREAL_1:9;
a - b <= s0 - b by A11, XREAL_1:9;
then (a - b) + (a - b) <= (s0 - b) + (s0 - b) by XREAL_1:7;
then A33: ((a - b) + (a - b)) - (a - b) <= ((s0 - b) + (s0 - b)) - (a - b) by XREAL_1:9;
(g2 . O) `1 = ((2 / (b - a)) * s0) + (1 - ((2 * b) / (b - a))) by A24, EUCLID:52
.= ((s0 * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= ((s0 * 2) / (b - a)) + (((b - a) / (b - a)) - ((2 * b) / (b - a))) by A26, 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) ;
hence ( - 1 <= (g2 . O) `1 & (g2 . O) `1 <= 1 & - 1 <= (g2 . I) `1 & (g2 . I) `1 <= 1 ) by A26, A33, A28, A30, A29, A32, A31, XREAL_1:72; :: thesis: verum

end;

A34: now :: thesis: not rng f2 meets K0

assume rng f2 meets K0 ; :: thesis: contradiction
then consider x being object such that
A35: x in rng f2 and
A36: x in K0 by XBOOLE_0:3;
reconsider q = x as Point of (TOP-REAL 2) by A35;
consider p being Point of (TOP-REAL 2) such that
A37: p = q and
A38: - 1 < p `1 and
A39: p `1 < 1 and
A40: - 1 < p `2 and
A41: p `2 < 1 by A36;
consider z being object such that
A42: z in dom f2 and
A43: x = f2 . z by A35, FUNCT_1:def 3;
reconsider u = z as Point of I[01] by A42;
reconsider t = f . u as Point of (TOP-REAL 2) ;
A44: ((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 A26, 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) ;
A45: (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) . t = p by A37, A42, A43, FUNCT_1:12;
A46: ((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 A19, 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) ;
A47: (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;
then - 1 < ((2 / (d - c)) * (t `2)) + (1 - ((2 * d) / (d - c))) by A40, A45, EUCLID:52;
then (- 1) * (d - c) < (((2 * ((t `2) - d)) - (c - d)) / (d - c)) * (d - c) by A19, A46, XREAL_1:68;
then (- 1) * (d - c) < (2 * ((t `2) - d)) - (c - d) by A19, XCMPLX_1:87;
then ((- 1) * (d - c)) + (c - d) < ((2 * ((t `2) - d)) - (c - d)) + (c - d) by XREAL_1:8;
then (2 * (c - d)) / 2 < (2 * ((t `2) - d)) / 2 by XREAL_1:74;
then A48: c < t `2 by XREAL_1:9;
((2 / (d - c)) * (t `2)) + (1 - ((2 * d) / (d - c))) < 1 by A41, A47, A45, EUCLID:52;
then 1 * (d - c) > (((2 * ((t `2) - d)) - (c - d)) / (d - c)) * (d - c) by A19, A46, XREAL_1:68;
then 1 * (d - c) > (2 * ((t `2) - d)) - (c - d) by A19, XCMPLX_1:87;
then (1 * (d - c)) + (c - d) > ((2 * ((t `2) - d)) - (c - d)) + (c - d) by XREAL_1:8;
then 0 / 2 > (((t `2) - d) * 2) / 2 ;
then A49: 0 + d > t `2 by XREAL_1:19;
((2 / (b - a)) * (t `1)) + (1 - ((2 * b) / (b - a))) < 1 by A39, A47, A45, EUCLID:52;
then 1 * (b - a) > (((2 * ((t `1) - b)) - (a - b)) / (b - a)) * (b - a) by A26, A44, XREAL_1:68;
then 1 * (b - a) > (2 * ((t `1) - b)) - (a - b) by A26, XCMPLX_1:87;
then (1 * (b - a)) + (a - b) > ((2 * ((t `1) - b)) - (a - b)) + (a - b) by XREAL_1:8;
then 0 / 2 > (((t `1) - b) * 2) / 2 ;
then A50: 0 + b > t `1 by XREAL_1:19;
- 1 < ((2 / (b - a)) * (t `1)) + (1 - ((2 * b) / (b - a))) by A38, A47, A45, EUCLID:52;
then (- 1) * (b - a) < (((2 * ((t `1) - b)) - (a - b)) / (b - a)) * (b - a) by A26, A44, XREAL_1:68;
then (- 1) * (b - a) < (2 * ((t `1) - b)) - (a - b) by A26, XCMPLX_1:87;
then ((- 1) * (b - a)) + (a - b) < ((2 * ((t `1) - b)) - (a - b)) + (a - b) by XREAL_1:8;
then (2 * (a - b)) / 2 < (2 * ((t `1) - b)) / 2 by XREAL_1:74;
then a < t `1 by XREAL_1:9;
hence contradiction by A17, A50, A48, A49; :: thesis: verum

end;

A51: dom f = the carrier of I[01] by FUNCT_2:def 1;
then A52: f2 . I = (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) . (f . I) by FUNCT_1:13
.= |[(((2 / (b - a)) * b) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * ((f . I) `2)) + (1 - ((2 * d) / (d - c))))]| by A4, Def2 ;
then A53: (f2 . I) `1 = ((2 / (b - a)) * b) + (1 - ((2 * b) / (b - a))) by EUCLID:52
.= ((b * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= 1 ;
A54: f2 . O = (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) . (f . O) by A51, FUNCT_1:13
.= |[(((2 / (b - a)) * a) + (1 - ((2 * b) / (b - a)))),(((2 / (d - c)) * ((f . O) `2)) + (1 - ((2 * d) / (d - c))))]| by A3, Def2 ;
then A55: (f2 . O) `1 = ((2 / (b - a)) * a) + (1 - ((2 * b) / (b - a))) by EUCLID:52
.= ((a * 2) / (b - a)) + (1 - ((2 * b) / (b - a)))
.= ((a * 2) / (b - a)) + (((b - a) / (b - a)) - ((2 * b) / (b - a))) by A26, 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 A26, XCMPLX_1:60 ;

A56: now :: thesis: not rng g2 meets K0

assume rng g2 meets K0 ; :: thesis: contradiction
then consider x being object such that
A57: x in rng g2 and
A58: x in K0 by XBOOLE_0:3;
reconsider q = x as Point of (TOP-REAL 2) by A57;
consider p being Point of (TOP-REAL 2) such that
A59: p = q and
A60: - 1 < p `1 and
A61: p `1 < 1 and
A62: - 1 < p `2 and
A63: p `2 < 1 by A58;
consider z being object such that
A64: z in dom g2 and
A65: x = g2 . z by A57, FUNCT_1:def 3;
reconsider u = z as Point of I[01] by A64;
reconsider t = g . u as Point of (TOP-REAL 2) ;
A66: ((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 A26, 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) ;
A67: (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) . t = p by A59, A64, A65, FUNCT_1:12;
A68: ((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 A19, 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) ;
A69: (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;
then - 1 < ((2 / (d - c)) * (t `2)) + (1 - ((2 * d) / (d - c))) by A62, A67, EUCLID:52;
then (- 1) * (d - c) < (((2 * ((t `2) - d)) - (c - d)) / (d - c)) * (d - c) by A19, A68, XREAL_1:68;
then (- 1) * (d - c) < (2 * ((t `2) - d)) - (c - d) by A19, XCMPLX_1:87;
then ((- 1) * (d - c)) + (c - d) < ((2 * ((t `2) - d)) - (c - d)) + (c - d) by XREAL_1:8;
then (2 * (c - d)) / 2 < (2 * ((t `2) - d)) / 2 by XREAL_1:74;
then A70: c < t `2 by XREAL_1:9;
((2 / (d - c)) * (t `2)) + (1 - ((2 * d) / (d - c))) < 1 by A63, A69, A67, EUCLID:52;
then 1 * (d - c) > (((2 * ((t `2) - d)) - (c - d)) / (d - c)) * (d - c) by A19, A68, XREAL_1:68;
then 1 * (d - c) > (2 * ((t `2) - d)) - (c - d) by A19, XCMPLX_1:87;
then (1 * (d - c)) + (c - d) > ((2 * ((t `2) - d)) - (c - d)) + (c - d) by XREAL_1:8;
then 0 / 2 > (((t `2) - d) * 2) / 2 ;
then A71: 0 + d > t `2 by XREAL_1:19;
((2 / (b - a)) * (t `1)) + (1 - ((2 * b) / (b - a))) < 1 by A61, A69, A67, EUCLID:52;
then 1 * (b - a) > (((2 * ((t `1) - b)) - (a - b)) / (b - a)) * (b - a) by A26, A66, XREAL_1:68;
then 1 * (b - a) > (2 * ((t `1) - b)) - (a - b) by A26, XCMPLX_1:87;
then (1 * (b - a)) + (a - b) > ((2 * ((t `1) - b)) - (a - b)) + (a - b) by XREAL_1:8;
then 0 / 2 > (((t `1) - b) * 2) / 2 ;
then A72: 0 + b > t `1 by XREAL_1:19;
- 1 < ((2 / (b - a)) * (t `1)) + (1 - ((2 * b) / (b - a))) by A60, A69, A67, EUCLID:52;
then (- 1) * (b - a) < (((2 * ((t `1) - b)) - (a - b)) / (b - a)) * (b - a) by A26, A66, XREAL_1:68;
then (- 1) * (b - a) < (2 * ((t `1) - b)) - (a - b) by A26, XCMPLX_1:87;
then ((- 1) * (b - a)) + (a - b) < ((2 * ((t `1) - b)) - (a - b)) + (a - b) by XREAL_1:8;
then (2 * (a - b)) / 2 < (2 * ((t `1) - b)) / 2 by XREAL_1:74;
then a < t `1 by XREAL_1:9;
hence contradiction by A18, A72, A70, A71; :: thesis: verum

end;

A73: ( - 1 <= (f2 . O) `2 & (f2 . O) `2 <= 1 & - 1 <= (f2 . I) `2 & (f2 . I) `2 <= 1 )

proof

reconsider s1 = (f . I) `2 as Real ;
reconsider s0 = (f . O) `2 as Real ;
A74: (c - d) / (d - c) = (- (d - c)) / (d - c)
.= - ((d - c) / (d - c))
.= - 1 by A19, XCMPLX_1:60 ;
A75: (f2 . I) `2 = ((2 / (d - c)) * s1) + (1 - ((2 * d) / (d - c))) by A52, EUCLID:52
.= ((s1 * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= ((s1 * 2) / (d - c)) + (((d - c) / (d - c)) - ((2 * d) / (d - c))) by A19, 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) ;
d - d >= s0 - d by A6, XREAL_1:9;
then (0 + (d - d)) - (c - d) >= ((s0 - d) + (s0 - d)) - (c - d) by XREAL_1:9;
then A76: (d - c) / (d - c) >= (((s0 - d) + (s0 - d)) - (c - d)) / (d - c) by A19, XREAL_1:72;
d - d >= s1 - d by A8, XREAL_1:9;
then A77: (0 + (d - d)) - (c - d) >= ((s1 - d) + (s1 - d)) - (c - d) by XREAL_1:9;
c - d <= s1 - d by A7, XREAL_1:9;
then (c - d) + (c - d) <= (s1 - d) + (s1 - d) by XREAL_1:7;
then A78: ((c - d) + (c - d)) - (c - d) <= ((s1 - d) + (s1 - d)) - (c - d) by XREAL_1:9;
c - d <= s0 - d by A5, XREAL_1:9;
then (c - d) + (c - d) <= (s0 - d) + (s0 - d) by XREAL_1:7;
then A79: ((c - d) + (c - d)) - (c - d) <= ((s0 - d) + (s0 - d)) - (c - d) by XREAL_1:9;
(f2 . O) `2 = ((2 / (d - c)) * s0) + (1 - ((2 * d) / (d - c))) by A54, EUCLID:52
.= ((s0 * 2) / (d - c)) + (1 - ((2 * d) / (d - c)))
.= ((s0 * 2) / (d - c)) + (((d - c) / (d - c)) - ((2 * d) / (d - c))) by A19, 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) ;
hence ( - 1 <= (f2 . O) `2 & (f2 . O) `2 <= 1 & - 1 <= (f2 . I) `2 & (f2 . I) `2 <= 1 ) by A19, A79, A74, A76, A75, A78, A77, XREAL_1:72; :: thesis: verum

end;

set y = the Element of (rng f2) /\ (rng g2);
2 / (b - a) > 0 by A26, XREAL_1:139;
then A80: AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c)))) is one-to-one by A20, Th44;
then ( f2 is one-to-one & g2 is one-to-one ) by A2, FUNCT_1:24;
then rng f2 meets rng g2 by A1, A2, A55, A53, A25, A23, A73, A27, A34, A56, Th42;
then A81: (rng f2) /\ (rng g2) <> {} ;
then the Element of (rng f2) /\ (rng g2) in rng f2 by XBOOLE_0:def 4;
then consider x being object such that
A82: x in dom f2 and
A83: the Element of (rng f2) /\ (rng g2) = f2 . x by FUNCT_1:def 3;
dom f2 c= dom f by RELAT_1:25;
then A84: f . x in rng f by A82, FUNCT_1:3;
the Element of (rng f2) /\ (rng g2) in rng g2 by A81, XBOOLE_0:def 4;
then consider x2 being object such that
A85: x2 in dom g2 and
A86: the Element of (rng f2) /\ (rng g2) = g2 . x2 by FUNCT_1:def 3;
A87: the Element of (rng f2) /\ (rng g2) = (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) . (g . x2) by A85, A86, FUNCT_1:12;
dom g2 c= dom g by RELAT_1:25;
then A88: g . x2 in rng g by A85, FUNCT_1:3;
( dom (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) = the carrier of (TOP-REAL 2) & the Element of (rng f2) /\ (rng g2) = (AffineMap ((2 / (b - a)),(1 - ((2 * b) / (b - a))),(2 / (d - c)),(1 - ((2 * d) / (d - c))))) . (f . x) ) by A82, A83, FUNCT_1:12, FUNCT_2:def 1;
then f . x = g . x2 by A80, A87, A84, A88, FUNCT_1:def 4;
then (rng f) /\ (rng g) <> {} by A84, A88, XBOOLE_0:def 4;
hence rng f meets rng g ; :: thesis: verum