for a, b being Point of (TOP-REAL 2)
for f being Path of a,b
for P being non empty compact SubSpace of TOP-REAL 2
for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds
g is being_homeomorphism by COMPTS_1:17, PRE_TOPC:27;