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 )
A1: dom g = [#] I[01] by FUNCT_2:def 1;
assume ( f is one-to-one & g = f & [#] P = rng f ) ; :: thesis: g is being_homeomorphism
hence g is being_homeomorphism by A1, COMPTS_1:17, PRE_TOPC:27; :: thesis: verum