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 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)))) & (f . I) `1 = b holds
((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 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)))) & (f . I) `1 = b holds
((h * f) . I) `1 = 1
let f be Function of I[01],(TOP-REAL 2); for 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)))) & (f . I) `1 = b holds
((h * f) . I) `1 = 1
let I be Point of I[01]; ( a < b & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . I) `1 = b implies ((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:
(f . I) `1 = b
; ((h * f) . I) `1 = 1
A4:
b - a > 0
by A1, XREAL_1:50;
dom f = the carrier of I[01]
by FUNCT_2:def 1;
then A5:
(h * f) . I = h . (f . I)
by FUNCT_1:13;
A6:
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;
((2 / (b - a)) * ((f . I) `1)) + (- ((b + a) / (b - a))) =
((2 * b) / (b - a)) + (- ((b + a) / (b - a)))
by A3, 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 A4, XCMPLX_1:60
;
hence
((h * f) . I) `1 = 1
by A5, A6, EUCLID:52; verum