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