let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y
for P being non empty Subset of Y st X is compact & Y is T_2 & f is continuous & f is one-to-one & P = rng f holds
ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism )

let f be Function of X,Y; :: thesis: for P being non empty Subset of Y st X is compact & Y is T_2 & f is continuous & f is one-to-one & P = rng f holds
ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism )

let P be non empty Subset of Y; :: thesis: ( X is compact & Y is T_2 & f is continuous & f is one-to-one & P = rng f implies ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism ) )

assume that
A1: X is compact and
A2: Y is T_2 and
A3: ( f is continuous & f is one-to-one ) and
A4: P = rng f ; :: thesis: ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism )

( the carrier of (Y | P) = P & dom f = the carrier of X ) by ;
then reconsider f2 = f as Function of X,(Y | P) by ;
A5: ( dom f2 = [#] X & f2 is continuous ) by ;
( rng f2 = [#] (Y | P) & Y | P is T_2 ) by ;
hence ex f1 being Function of X,(Y | P) st
( f = f1 & f1 is being_homeomorphism ) by ; :: thesis: verum