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) st a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & f is continuous & f is one-to-one holds
( h * f is continuous & h * f is one-to-one )
let h be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: for f being Function of I[01] ,(TOP-REAL 2) st a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & f is continuous & f is one-to-one holds
( h * f is continuous & h * f is one-to-one )
let f be Function of I[01] ,(TOP-REAL 2); :: thesis: ( a < b & c < d & h = AffineMap (2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c))) & f is continuous & f is one-to-one implies ( h * f is continuous & h * f is one-to-one ) )
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 is continuous & f is one-to-one ) ; :: thesis: ( h * f is continuous & h * f is one-to-one )
then b - a > 0 by XREAL_1:52;
then A2: 2 / (b - a) > 0 by XREAL_1:141;
d - c > 0 by A1, XREAL_1:52;
then 2 / (d - c) > 0 by XREAL_1:141;
then h is being_homeomorphism by A1, A2, Th51;
then h is one-to-one by TOPS_2:def 5;
hence ( h * f is continuous & h * f is one-to-one ) by A1, FUNCT_1:46; :: thesis: verum