consider f being Function of I[01],(Closed-Interval-TSpace (((2 * 0) + (- 1)),((2 * 1) + (- 1)))) such that
A1: f is being_homeomorphism and
A2: for r being Real st r in [.0,1.] holds
f . r = (2 * r) + (- 1) by Th36, TOPMETR:20;
A3: 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 A2
.= (2 * r) - 1 ;
:: thesis: verum

end;

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