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 FUNCT_2:def 1, PRE_TOPC:8;

then reconsider f2 = f as Function of X,(Y | P) by A4, FUNCT_2:1;

A5: ( dom f2 = [#] X & f2 is continuous ) by A3, Th44, FUNCT_2:def 1;

( rng f2 = [#] (Y | P) & Y | P is T_2 ) by A2, A4, PRE_TOPC:def 5, TOPMETR:2;

hence ex f1 being Function of X,(Y | P) st

( f = f1 & f1 is being_homeomorphism ) by A1, A3, A5, COMPTS_1:17; :: thesis: verum

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 FUNCT_2:def 1, PRE_TOPC:8;

then reconsider f2 = f as Function of X,(Y | P) by A4, FUNCT_2:1;

A5: ( dom f2 = [#] X & f2 is continuous ) by A3, Th44, FUNCT_2:def 1;

( rng f2 = [#] (Y | P) & Y | P is T_2 ) by A2, A4, PRE_TOPC:def 5, TOPMETR:2;

hence ex f1 being Function of X,(Y | P) st

( f = f1 & f1 is being_homeomorphism ) by A1, A3, A5, COMPTS_1:17; :: thesis: verum