let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is one-to-one & f is onto holds
( f is open iff f " is continuous )
let f be Function of S,T; :: thesis: ( f is one-to-one & f is onto implies ( f is open iff f " is continuous ) )
assume A1: f is one-to-one ; :: thesis: ( not f is onto or ( f is open iff f " is continuous ) )
assume f is onto ; :: thesis: ( f is open iff f " is continuous )
then A2: rng f = [#] T by FUNCT_2:def 3;
then rng (f " ) = [#] S by A1, TOPS_2:62;
then A3: f " is onto by FUNCT_2:def 3;
A4: f " is one-to-one by A1, A2, TOPS_2:63;
(f " ) " = f by A1, A2, TOPS_2:64;
hence ( f is open iff f " is continuous ) by A3, A4, Th34; :: thesis: verum