let X, Y be non empty TopSpace; :: thesis: for f being continuous Function of X,Y st f is one-to-one & f is onto holds
( f is being_homeomorphism iff f is closed )
let f be continuous Function of X,Y; :: thesis: ( f is one-to-one & f is onto implies ( f is being_homeomorphism iff f is closed ) )
assume A1: ( f is one-to-one & f is onto ) ; :: thesis: ( f is being_homeomorphism iff f is closed )

hereby :: thesis: ( f is closed implies f is being_homeomorphism )

assume A2: f is being_homeomorphism ; :: thesis: f is closed
thus f is closed :: thesis: verum

proof

let A be Subset of X; :: according to JORDAN24:def 4 :: thesis: ( A is closed implies f .: A is closed )
thus ( A is closed implies f .: A is closed ) by A2, TOPS_2:58; :: thesis: verum

end;

end;

assume A3: for A being Subset of X st A is closed holds
f .: A is closed ; :: according to JORDAN24:def 4 :: thesis: f is being_homeomorphism
A4: ( [#] X = the carrier of X & [#] Y = the carrier of Y ) ;
A5: dom f = the carrier of X by FUNCT_2:def 1;

A6: now

let A be Subset of X; :: thesis: ( f .: A is closed implies A is closed )
assume f .: A is closed ; :: thesis: A is closed
then f " (f .: A) is closed by PRE_TOPC:def 6;
hence A is closed by A1, A5, FUNCT_1:94; :: thesis: verum

end;

rng f = the carrier of Y by A1, FUNCT_2:def 3;
hence f is being_homeomorphism by A1, A3, A5, A4, A6, TOPS_2:58; :: thesis: verum