let TS be TopSpace; :: thesis: for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is Hausdorff & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous holds
f is being_homeomorphism
let SS be non empty TopSpace; :: thesis: for f being Function of TS,SS st TS is compact & SS is Hausdorff & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous holds
f is being_homeomorphism
let f be Function of TS,SS; :: thesis: ( TS is compact & SS is Hausdorff & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous implies f is being_homeomorphism )
assume that
A1: TS is compact and
A2: SS is Hausdorff and
A3: dom f = [#] TS and
A4: rng f = [#] SS and
A5: f is one-to-one and
A6: f is continuous ; :: thesis: f is being_homeomorphism
for P being Subset of TS holds
( P is closed iff f .: P is closed )

proof

let P be Subset of TS; :: thesis: ( P is closed iff f .: P is closed )
dom f = [#] TS by FUNCT_2:def 1;
then A7: P c= f " (f .: P) by FUNCT_1:146;
thus ( P is closed implies f .: P is closed ) by A1, A2, A4, A6, Th25; :: thesis: ( f .: P is closed implies P is closed )
assume f .: P is closed ; :: thesis: P is closed
then A8: f " (f .: P) is closed by A6, PRE_TOPC:def 12;
f " (f .: P) c= P by A5, FUNCT_1:152;
hence P is closed by A8, A7, XBOOLE_0:def 10; :: thesis: verum

end;

hence f is being_homeomorphism by A3, A4, A5, TOPS_2:72; :: thesis: verum