let T be TopStruct ; :: thesis:
let S be non empty TopStruct ; :: thesis:
let f be Function of T,S; :: thesis:

hereby :: thesis:

assume A1: f is being_homeomorphism ; :: thesis:
hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) ; :: thesis:
let P be Subset of T; :: thesis:
A3: f " is continuous by A1;

hereby :: thesis:

assume A4: P is closed ; :: thesis:
f is onto by A2, FUNCT_2:def 3;
then (f ") " P = (f ") " P by A2, Def4
.= f .: P by A2, FUNCT_1:84 ;
hence f .: P is closed by A3, A4; :: thesis:

end;

assume A5: f .: P is closed ; :: thesis:
f is continuous by A1;
then A6: f " (f .: P) is closed by A5;
dom f = [#] T by FUNCT_2:def 1;
then A7: P c= f " (f .: P) by FUNCT_1:76;
f " (f .: P) c= P by A2, FUNCT_1:82;
hence P is closed by A6, A7, XBOOLE_0:def 10; :: thesis:

end;

assume that
A8: dom f = [#] T and
A9: rng f = [#] S and
A10: f is one-to-one ; :: thesis:
assume A11: for P being Subset of T holds
( P is closed iff f .: P is closed ) ; :: thesis:
A12: f is continuous

let B be Subset of S; :: according to PRE_TOPC:def 6 :: thesis:
assume A13: B is closed ; :: thesis:
set D = f " B;
B = f .: (f " B) by A9, FUNCT_1:77;
hence f " B is closed by A11, A13; :: thesis:

end;

f " is continuous

let B be Subset of T; :: according to PRE_TOPC:def 6 :: thesis:
assume A14: B is closed ; :: thesis:
f is onto by A9, FUNCT_2:def 3;
then (f ") " B = (f ") " B by A10, Def4
.= f .: B by A10, FUNCT_1:84 ;
hence (f ") " B is closed by A11, A14; :: thesis:

end;

hence f is being_homeomorphism by A8, A9, A10, A12; :: thesis: