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

proof

let r be Real; :: thesis: ( r in [.0 ,1.] implies f . r = (2 * r) - 1 )
assume r in [.0 ,1.] ; :: thesis: f . r = (2 * r) - 1
hence f . r = (2 * r) + (- 1) by A1
.= (2 * r) - 1 ;
:: thesis: verum

end;

then A3: f . 0 = (2 * 0 ) - 1 by Lm1
.= - 1 ;
1 in [.0 ,1.] by XXREAL_1:1;
then f . 1 = (2 * 1) - 1 by A2
.= 1 ;
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, A3; :: thesis: verum