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) st a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & rng f c= closed_inside_of_rectangle a,b,c,d holds
rng (h * f) c= closed_inside_of_rectangle (- 1),1,(- 1),1
let h be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: for f being Function of I[01] ,(TOP-REAL 2) st a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & rng f c= closed_inside_of_rectangle a,b,c,d holds
rng (h * f) c= closed_inside_of_rectangle (- 1),1,(- 1),1
let f be Function of I[01] ,(TOP-REAL 2); :: thesis: ( a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & rng f c= closed_inside_of_rectangle a,b,c,d implies rng (h * f) c= closed_inside_of_rectangle (- 1),1,(- 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))) & rng f c= closed_inside_of_rectangle a,b,c,d ) ; :: thesis: rng (h * f) c= closed_inside_of_rectangle (- 1),1,(- 1),1
then A2: b - a > 0 by XREAL_1:52;
then A3: 2 / (b - a) > 0 by XREAL_1:141;
A4: d - c > 0 by A1, XREAL_1:52;
then A5: 2 / (d - c) > 0 by XREAL_1:141;
A6: ((- 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
.= (((a + a) / (b - a)) / 2) * (b - a) by XCMPLX_1:83
.= ((b - a) * ((a + a) / (b - a))) / 2
.= (a + a) / 2 by A2, XCMPLX_1:88
.= a ;
A7: (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 + b) / (b - a)) / 2) * (b - a) by XCMPLX_1:83
.= ((b - a) * ((b + b) / (b - a))) / 2
.= (b + b) / 2 by A2, XCMPLX_1:88
.= b ;
A8: ((- 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 A4, XCMPLX_1:114
.= (((c + c) / (d - c)) / 2) * (d - c) by XCMPLX_1:83
.= ((d - c) * ((c + c) / (d - c))) / 2
.= (c + c) / 2 by A4, XCMPLX_1:88
.= c ;
A9: (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 A4, XCMPLX_1:114
.= (((d + d) / (d - c)) / 2) * (d - c) by XCMPLX_1:83
.= ((d - c) * ((d + d) / (d - c))) / 2
.= (d + d) / 2 by A4, XCMPLX_1:88
.= d ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (h * f) or x in closed_inside_of_rectangle (- 1),1,(- 1),1 )
assume x in rng (h * f) ; :: thesis: x in closed_inside_of_rectangle (- 1),1,(- 1),1
then consider y being set such that
A10: ( y in dom (h * f) & x = (h * f) . y ) by FUNCT_1:def 5;
reconsider p0 = x as Point of (TOP-REAL 2) by A10, FUNCT_2:7;
reconsider t0 = y as Point of I[01] by A10;
A11: h . (f . t0) = |[(((2 / (b - a)) * ((f . t0) `1 )) + (- ((b + a) / (b - a)))),(((2 / (d - c)) * ((f . t0) `2 )) + (- ((d + c) / (d - c))))]| by A1, JGRAPH_2:def 2;
A12: (h * f) . t0 = h . (f . t0) by A10, FUNCT_1:22;
dom f = the carrier of I[01] by FUNCT_2:def 1;
then f . t0 in rng f by FUNCT_1:def 5;
then f . t0 in closed_inside_of_rectangle a,b,c,d by A1;
then f . t0 in { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } by JGRAPH_6:def 2;
then consider p being Point of (TOP-REAL 2) such that
A13: ( f . t0 = p & a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) ;
(2 / (d - c)) * (((- 1) - (- ((d + c) / (d - c)))) / (2 / (d - c))) <= (2 / (d - c)) * ((f . t0) `2 ) by A5, A8, A13, XREAL_1:66;
then (- 1) - (- ((d + c) / (d - c))) <= (2 / (d - c)) * ((f . t0) `2 ) by A5, XCMPLX_1:88;
then ((- 1) - (- ((d + c) / (d - c)))) + (- ((d + c) / (d - c))) <= ((2 / (d - c)) * ((f . t0) `2 )) + (- ((d + c) / (d - c))) by XREAL_1:8;
then A14: - 1 <= p0 `2 by A10, A11, A12, EUCLID:56;
(2 / (d - c)) * ((1 - (- ((d + c) / (d - c)))) / (2 / (d - c))) >= (2 / (d - c)) * ((f . t0) `2 ) by A5, A9, A13, XREAL_1:66;
then 1 - (- ((d + c) / (d - c))) >= (2 / (d - c)) * ((f . t0) `2 ) by A5, XCMPLX_1:88;
then (1 - (- ((d + c) / (d - c)))) + (- ((d + c) / (d - c))) >= ((2 / (d - c)) * ((f . t0) `2 )) + (- ((d + c) / (d - c))) by XREAL_1:8;
then A15: p0 `2 <= 1 by A10, A11, A12, EUCLID:56;
(2 / (b - a)) * (((- 1) - (- ((b + a) / (b - a)))) / (2 / (b - a))) <= (2 / (b - a)) * ((f . t0) `1 ) by A3, A6, A13, XREAL_1:66;
then (- 1) - (- ((b + a) / (b - a))) <= (2 / (b - a)) * ((f . t0) `1 ) by A3, XCMPLX_1:88;
then ((- 1) - (- ((b + a) / (b - a)))) + (- ((b + a) / (b - a))) <= ((2 / (b - a)) * ((f . t0) `1 )) + (- ((b + a) / (b - a))) by XREAL_1:8;
then A16: - 1 <= p0 `1 by A10, A11, A12, EUCLID:56;
(2 / (b - a)) * ((1 - (- ((b + a) / (b - a)))) / (2 / (b - a))) >= (2 / (b - a)) * ((f . t0) `1 ) by A3, A7, A13, XREAL_1:66;
then 1 - (- ((b + a) / (b - a))) >= (2 / (b - a)) * ((f . t0) `1 ) by A3, XCMPLX_1:88;
then (1 - (- ((b + a) / (b - a)))) + (- ((b + a) / (b - a))) >= ((2 / (b - a)) * ((f . t0) `1 )) + (- ((b + a) / (b - a))) by XREAL_1:8;
then p0 `1 <= 1 by A10, A11, A12, EUCLID:56;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( - 1 <= p2 `1 & p2 `1 <= 1 & - 1 <= p2 `2 & p2 `2 <= 1 ) } by A14, A15, A16;
hence x in closed_inside_of_rectangle (- 1),1,(- 1),1 by JGRAPH_6:def 2; :: thesis: verum