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 )
thus ( f is being_homeomorphism implies f is closed ) by TOPS_2:58; :: thesis: ( f is closed implies f is being_homeomorphism )
assume A2: 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
A3: ( [#] X = the carrier of X & [#] Y = the carrier of Y ) ;
A4: dom f = the carrier of X by FUNCT_2:def 1;
A5: now :: thesis: for A being Subset of X st f .: A is closed holds
A is closed
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, A4, FUNCT_1:94; :: thesis: verum
end;
thus f is being_homeomorphism by A1, A2, A4, A3, A5, TOPS_2:58; :: thesis: verum