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) 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 that
A1: a < b and
A2: c < d and
A3: h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) and
A4: ( f is continuous & f is one-to-one ) ; :: thesis: ( h * f is continuous & h * f is one-to-one )
d - c > 0 by A2, XREAL_1:50;
then A5: 2 / (d - c) > 0 by XREAL_1:139;
b - a > 0 by A1, XREAL_1:50;
then 2 / (b - a) > 0 by XREAL_1:139;
then h is being_homeomorphism by A3, A5, Th51;
then h is one-to-one by TOPS_2:def 5;
hence ( h * f is continuous & h * f is one-to-one ) by A3, A4, FUNCT_1:24; :: thesis: verum