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)))) & 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); 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); 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]; ( 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
; ( - 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
.=
(d - c) * (((c + c) / (d - c)) / 2)
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
.=
((d + 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:68;
then A20:
((2 / (b - a)) * a) + (- ((b + a) / (b - a))) < ((2 / (b - a)) * ((f . I) `1)) + (- ((b + a) / (b - a)))
by XREAL_1:8;
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
.=
((b + 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
.=
((a + 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, A13, A21, A12, A11, A19, A20, EUCLID:52; verum