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 )