consider f being Function of I[01] ,(Closed-Interval-TSpace (((- 2) * 1) + 1),(((- 2) * 0 ) + 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 Th40, TOPMETR:27;
1 in [.0 ,1.]
by XXREAL_1:1;
then A3:
f . 1 = - 1
by A2;
f . 0 = ((- 2) * 0 ) + 1
by A2, Lm1;
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; verum