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