let a, b, c, d be real number ; :: thesis: 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 & 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); :: thesis: for f being Function of I[01] ,(TOP-REAL 2)
for 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))) & (f . I) `2 = c holds
((h * f) . I) `2 = - 1
let f be Function of I[01] ,(TOP-REAL 2); :: thesis: for 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))) & (f . I) `2 = c holds
((h * f) . I) `2 = - 1
let I be Point of I[01] ; :: thesis: ( a < b & 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 A1: ( a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & (f . I) `2 = c ) ; :: thesis: ((h * f) . I) `2 = - 1
then A2: d - c > 0 by XREAL_1:52;
dom f = the carrier of I[01] by FUNCT_2:def 1;
then A3: (h * f) . I = h . (f . I) by FUNCT_1:23;
A4: h . (f . I) = |[(((2 / (b - a)) * ((f . I) `1 )) + (- ((b + a) / (b - a)))),(((2 / (d - c)) * ((f . I) `2 )) + (- ((d + c) / (d - c))))]| by A1, JGRAPH_2:def 2;
((2 / (d - c)) * ((f . I) `2 )) + (- ((d + c) / (d - c))) = ((2 * c) / (d - c)) + (- ((d + c) / (d - c))) by A1, XCMPLX_1:75
.= ((2 * c) / (d - c)) + ((- (d + c)) / (d - c)) by XCMPLX_1:188
.= ((c + c) + (- (d + c))) / (d - c) by XCMPLX_1:63
.= (- (d - c)) / (d - c)
.= - 1 by A2, XCMPLX_1:198 ;
hence ((h * f) . I) `2 = - 1 by A3, A4, EUCLID:56; :: thesis: verum