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