let a, b be Point of (TOP-REAL 2); :: thesis: 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
let f be Path of a,b; :: thesis: 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
let P be non empty compact SubSpace of TOP-REAL 2; :: thesis: for g being Function of I[01] ,P st f is one-to-one & g = f & [#] P = rng f holds
g is being_homeomorphism
let g be Function of I[01] ,P; :: thesis: ( f is one-to-one & g = f & [#] P = rng f implies g is being_homeomorphism )
assume A1: ( f is one-to-one & g = f & [#] P = rng f ) ; :: thesis: g is being_homeomorphism
dom g = [#] I[01] by FUNCT_2:def 1;
hence g is being_homeomorphism by A1, COMPTS_1:26, PRE_TOPC:57; :: thesis: verum