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 c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . I) `2 = c holds
((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 I being Point of I[01] st c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . I) `2 = c holds
((h * f) . I) `2 = - 1
let f be Function of I[01],(TOP-REAL 2); for I being Point of I[01] st c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . I) `2 = c holds
((h * f) . I) `2 = - 1
let I be Point of I[01]; ( c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . I) `2 = c implies ((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:
c < d
and
A2:
h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))))
and
A3:
(f . I) `2 = c
; ((h * f) . I) `2 = - 1
A4:
d - c > 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 / (d - c)) * ((f . I) `2)) + (- ((d + c) / (d - c))) =
((2 * c) / (d - c)) + (- ((d + c) / (d - c)))
by A3, XCMPLX_1:74
.=
((2 * c) / (d - c)) + ((- (d + c)) / (d - c))
by XCMPLX_1:187
.=
((c + c) + (- (d + c))) / (d - c)
by XCMPLX_1:62
.=
(- (d - c)) / (d - c)
.=
- 1
by A4, XCMPLX_1:197
;
hence
((h * f) . I) `2 = - 1
by A5, A6, EUCLID:52; verum