consider f being Function of I[01] ,(Closed-Interval-TSpace (((- 2) * 1) + 1),(((- 2) * 0 ) + 1)) such that
A1: ( f is being_homeomorphism & ( for r being Real st r in [.0 ,1.] holds
f . r = ((- 2) * r) + 1 ) ) by Th40, TOPMETR:27;
A2: f . 0 = ((- 2) * 0 ) + 1 by A1, Lm1;
1 in [.0 ,1.] by XXREAL_1:1;
then f . 1 = - 1 by A1;
hence ex f being Function of I[01] ,(Closed-Interval-TSpace (- 1),1) st
( f is being_homeomorphism & ( for r being Real st r in [.0 ,1.] holds
f . r = ((- 2) * r) + 1 ) & f . 0 = 1 & f . 1 = - 1 ) by A1, A2; :: thesis: verum