let a, b, c, d be Real; :: 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)))) & c <= (f . O) `2 & (f . O) `2 <= d & a <= (f . I) `1 & (f . I) `1 <= b holds
( - 1 <= ((h * f) . O) `2 & ((h * f) . O) `2 <= 1 & - 1 <= ((h * f) . I) `1 & ((h * f) . I) `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)))) & c <= (f . O) `2 & (f . O) `2 <= d & a <= (f . I) `1 & (f . I) `1 <= b holds
( - 1 <= ((h * f) . O) `2 & ((h * f) . O) `2 <= 1 & - 1 <= ((h * f) . I) `1 & ((h * f) . I) `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)))) & c <= (f . O) `2 & (f . O) `2 <= d & a <= (f . I) `1 & (f . I) `1 <= b holds
( - 1 <= ((h * f) . O) `2 & ((h * f) . O) `2 <= 1 & - 1 <= ((h * f) . I) `1 & ((h * f) . I) `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)))) & c <= (f . O) `2 & (f . O) `2 <= d & a <= (f . I) `1 & (f . I) `1 <= b implies ( - 1 <= ((h * f) . O) `2 & ((h * f) . O) `2 <= 1 & - 1 <= ((h * f) . I) `1 & ((h * f) . I) `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 that
A1: a < b and
A2: c < d and
A3: h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) and
A4: c <= (f . O) `2 and
A5: (f . O) `2 <= d and
A6: a <= (f . I) `1 and
A7: (f . I) `1 <= b ; :: thesis: ( - 1 <= ((h * f) . O) `2 & ((h * f) . O) `2 <= 1 & - 1 <= ((h * f) . I) `1 & ((h * f) . I) `1 <= 1 )
A8: h . (f . O) = |[(((2 / (b - a)) * ((f . O) `1)) + (- ((b + a) / (b - a)))),(((2 / (d - c)) * ((f . O) `2)) + (- ((d + c) / (d - c))))]| by A3, JGRAPH_2:def 2;
A9: d - c > 0 by A2, XREAL_1:50;
then A10: 2 / (d - c) > 0 by XREAL_1:139;
then (2 / (d - c)) * d >= (2 / (d - c)) * ((f . O) `2) by A5, XREAL_1:64;
then A11: ((2 / (d - c)) * d) + (- ((d + c) / (d - c))) >= ((2 / (d - c)) * ((f . O) `2)) + (- ((d + c) / (d - c))) by XREAL_1:6;
((- 1) - (- ((d + c) / (d - c)))) / (2 / (d - c)) = ((- 1) + ((d + c) / (d - c))) / (2 / (d - c))
.= ((((- 1) * (d - c)) + (d + c)) / (d - c)) / (2 / (d - c)) by A9, XCMPLX_1:113
.= (((c + c) / (d - c)) / 2) * (d - c) by XCMPLX_1:82
.= ((d - c) * ((c + c) / (d - c))) / 2
.= (c + c) / 2 by A9, XCMPLX_1:87
.= c ;
then (2 / (d - c)) * (((- 1) - (- ((d + c) / (d - c)))) / (2 / (d - c))) <= (2 / (d - c)) * ((f . O) `2) by A4, A10, XREAL_1:64;
then (- 1) - (- ((d + c) / (d - c))) <= (2 / (d - c)) * ((f . O) `2) by A10, XCMPLX_1:87;
then A12: ((- 1) - (- ((d + c) / (d - c)))) + (- ((d + c) / (d - c))) <= ((2 / (d - c)) * ((f . O) `2)) + (- ((d + c) / (d - c))) by XREAL_1:6;
A13: ((2 / (d - c)) * d) + (- ((d + c) / (d - c))) = ((2 * d) / (d - c)) + (- ((d + c) / (d - c))) by XCMPLX_1:74
.= ((2 * d) / (d - c)) + ((- (d + c)) / (d - c)) by XCMPLX_1:187
.= ((2 * d) + (- (d + c))) / (d - c) by XCMPLX_1:62
.= 1 by A9, XCMPLX_1:60 ;
A14: h . (f . I) = |[(((2 / (b - a)) * ((f . I) `1)) + (- ((b + a) / (b - a)))),(((2 / (d - c)) * ((f . I) `2)) + (- ((d + c) / (d - c))))]| by A3, JGRAPH_2:def 2;
A15: dom f = the carrier of I[01] by FUNCT_2:def 1;
then A16: (h * f) . I = h . (f . I) by FUNCT_1:13;
A17: b - a > 0 by A1, XREAL_1:50;
then A18: 2 / (b - a) > 0 by XREAL_1:139;
then (2 / (b - a)) * b >= (2 / (b - a)) * ((f . I) `1) by A7, XREAL_1:64;
then A19: ((2 / (b - a)) * b) + (- ((b + a) / (b - a))) >= ((2 / (b - a)) * ((f . I) `1)) + (- ((b + a) / (b - a))) by XREAL_1:6;
(2 / (b - a)) * a <= (2 / (b - a)) * ((f . I) `1) by A6, A18, XREAL_1:64;
then A20: ((2 / (b - a)) * a) + (- ((b + a) / (b - a))) <= ((2 / (b - a)) * ((f . I) `1)) + (- ((b + a) / (b - a))) by XREAL_1:7;
A21: ((2 / (b - a)) * b) + (- ((b + a) / (b - a))) = ((2 * b) / (b - a)) + (- ((b + a) / (b - a))) by XCMPLX_1:74
.= ((2 * b) / (b - a)) + ((- (b + a)) / (b - a)) by XCMPLX_1:187
.= ((2 * b) + (- (b + a))) / (b - a) by XCMPLX_1:62
.= 1 by A17, XCMPLX_1:60 ;
A22: ((2 / (b - a)) * a) + (- ((b + a) / (b - a))) = ((2 * a) / (b - a)) + (- ((b + a) / (b - a))) by XCMPLX_1:74
.= ((2 * a) / (b - a)) + ((- (b + a)) / (b - a)) by XCMPLX_1:187
.= ((2 * a) + (- (b + a))) / (b - a) by XCMPLX_1:62
.= (- (b - a)) / (b - a)
.= - 1 by A17, XCMPLX_1:197 ;
(h * f) . O = h . (f . O) by A15, FUNCT_1:13;
hence ( - 1 <= ((h * f) . O) `2 & ((h * f) . O) `2 <= 1 & - 1 <= ((h * f) . I) `1 & ((h * f) . I) `1 <= 1 ) by A16, A8, A14, A22, A21, A13, A12, A11, A19, A20, EUCLID:52; :: thesis: verum