let TS be TopSpace; :: thesis: for SS being non empty TopSpace
for f being Function of TS,SS st TS is compact & SS is T_2 & 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 T_2 & 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 T_2 & 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 T_2 and
A3: rng f = [#] SS and
A4: f is one-to-one and
A5: f is continuous ; :: thesis: f is being_homeomorphism
A6: dom f = [#] TS by FUNCT_2:def 1;
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 )
A7: P c= f " (f .: P) by A6, FUNCT_1:76;
thus ( P is closed implies f .: P is closed ) by A1, A2, A3, A5, Th16; :: 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 A5;
f " (f .: P) c= P by A4, FUNCT_1:82;
hence P is closed by A8, A7, XBOOLE_0:def 10; :: thesis: verum

end;

hence f is being_homeomorphism by A6, A3, A4, TOPS_2:58; :: thesis: verum