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