theorem Th16: :: JORDAN7:16

for n being Nat
for P being non empty Subset of (TOP-REAL n)
for g being Function of I[01],(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds
ex f being Function of I[01],((TOP-REAL n) | P) st
( f = g & f is being_homeomorphism )