let a, b, c, d be real number ; :: thesis: for h being Function of (TOP-REAL 2),(TOP-REAL 2)
for f being Function of I[01] ,(TOP-REAL 2)
for O, I being Point of I[01] st a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & a < (f . I) `1 & (f . I) `1 < (f . O) `1 & (f . O) `1 <= b holds
( - 1 < ((h * f) . I) `1 & ((h * f) . I) `1 < ((h * f) . O) `1 & ((h * f) . O) `1 <= 1 )
let h be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: for f being Function of I[01] ,(TOP-REAL 2)
for O, I being Point of I[01] st a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & a < (f . I) `1 & (f . I) `1 < (f . O) `1 & (f . O) `1 <= b holds
( - 1 < ((h * f) . I) `1 & ((h * f) . I) `1 < ((h * f) . O) `1 & ((h * f) . O) `1 <= 1 )
let f be Function of I[01] ,(TOP-REAL 2); :: thesis: for O, I being Point of I[01] st a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & a < (f . I) `1 & (f . I) `1 < (f . O) `1 & (f . O) `1 <= b holds
( - 1 < ((h * f) . I) `1 & ((h * f) . I) `1 < ((h * f) . O) `1 & ((h * f) . O) `1 <= 1 )
let O, I be Point of I[01] ; :: thesis: ( a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & a < (f . I) `1 & (f . I) `1 < (f . O) `1 & (f . O) `1 <= b implies ( - 1 < ((h * f) . I) `1 & ((h * f) . I) `1 < ((h * f) . O) `1 & ((h * f) . O) `1 <= 1 ) )
set A = 2 / (b - a);
set B = - ((b + a) / (b - a));
set C = 2 / (d - c);
set D = - ((d + c) / (d - c));
assume A1: ( a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & a < (f . I) `1 & (f . I) `1 < (f . O) `1 & (f . O) `1 <= b ) ; :: thesis: ( - 1 < ((h * f) . I) `1 & ((h * f) . I) `1 < ((h * f) . O) `1 & ((h * f) . O) `1 <= 1 )
then A2: b - a > 0 by XREAL_1:52;
then A3: 2 / (b - a) > 0 by XREAL_1:141;
A4: dom f = the carrier of I[01] by FUNCT_2:def 1;
then A5: (h * f) . O = h . (f . O) by FUNCT_1:23;
A6: (h * f) . I = h . (f . I) by A4, FUNCT_1:23;
A7: h . (f . O) = |[(((2 / (b - a)) * ((f . O) `1 )) + (- ((b + a) / (b - a)))),(((2 / (d - c)) * ((f . O) `2 )) + (- ((d + c) / (d - c))))]| by A1, JGRAPH_2:def 2;
A8: h . (f . I) = |[(((2 / (b - a)) * ((f . I) `1 )) + (- ((b + a) / (b - a)))),(((2 / (d - c)) * ((f . I) `2 )) + (- ((d + c) / (d - c))))]| by A1, JGRAPH_2:def 2;
A9: (1 - (- ((b + a) / (b - a)))) / (2 / (b - a)) = (1 + ((b + a) / (b - a))) / (2 / (b - a))
.= (((1 * (b - a)) + (b + a)) / (b - a)) / (2 / (b - a)) by A2, XCMPLX_1:114
.= (b - a) * (((b + b) / (b - a)) / 2) by XCMPLX_1:83
.= ((b - a) * ((b + b) / (b - a))) / 2
.= (b + b) / 2 by A2, XCMPLX_1:88
.= b ;
A10: ((- 1) - (- ((b + a) / (b - a)))) / (2 / (b - a)) = ((- 1) + ((b + a) / (b - a))) / (2 / (b - a))
.= ((((- 1) * (b - a)) + (b + a)) / (b - a)) / (2 / (b - a)) by A2, XCMPLX_1:114
.= (b - a) * (((a + a) / (b - a)) / 2) by XCMPLX_1:83
.= ((b - a) * ((a + a) / (b - a))) / 2
.= (a + a) / 2 by A2, XCMPLX_1:88
.= a ;
(2 / (b - a)) * ((1 - (- ((b + a) / (b - a)))) / (2 / (b - a))) >= (2 / (b - a)) * ((f . O) `1 ) by A1, A3, A9, XREAL_1:66;
then 1 - (- ((b + a) / (b - a))) >= (2 / (b - a)) * ((f . O) `1 ) by A3, XCMPLX_1:88;
then A11: (1 - (- ((b + a) / (b - a)))) + (- ((b + a) / (b - a))) >= ((2 / (b - a)) * ((f . O) `1 )) + (- ((b + a) / (b - a))) by XREAL_1:8;
(2 / (b - a)) * (((- 1) - (- ((b + a) / (b - a)))) / (2 / (b - a))) < (2 / (b - a)) * ((f . I) `1 ) by A1, A3, A10, XREAL_1:70;
then (- 1) - (- ((b + a) / (b - a))) < (2 / (b - a)) * ((f . I) `1 ) by A3, XCMPLX_1:88;
then A12: ((- 1) - (- ((b + a) / (b - a)))) + (- ((b + a) / (b - a))) < ((2 / (b - a)) * ((f . I) `1 )) + (- ((b + a) / (b - a))) by XREAL_1:10;
(2 / (b - a)) * ((f . O) `1 ) > (2 / (b - a)) * ((f . I) `1 ) by A1, A3, XREAL_1:70;
then ((2 / (b - a)) * ((f . O) `1 )) + (- ((b + a) / (b - a))) > ((2 / (b - a)) * ((f . I) `1 )) + (- ((b + a) / (b - a))) by XREAL_1:10;
then ((2 / (b - a)) * ((f . O) `1 )) + (- ((b + a) / (b - a))) > ((h * f) . I) `1 by A6, A8, EUCLID:56;
hence ( - 1 < ((h * f) . I) `1 & ((h * f) . I) `1 < ((h * f) . O) `1 & ((h * f) . O) `1 <= 1 ) by A5, A6, A7, A8, A11, A12, EUCLID:56; :: thesis: verum