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 continuous iff f " is open )
let f be Function of S,T; :: thesis: ( f is one-to-one & f is onto implies ( f is continuous iff f " is open ) )
assume A1: f is one-to-one ; :: thesis: ( not f is onto or ( f is continuous iff f " is open ) )
A2: [#] T <> {} ;
assume f is onto ; :: thesis: ( f is continuous iff f " is open )
then rng f = [#] T by FUNCT_2:def 3;
then A3: f " = f " by A1, TOPS_2:def 4;
thus ( f is continuous implies f " is open ) :: thesis: ( f " is open implies f is continuous )

proof

assume A4: f is continuous ; :: thesis: f " is open
let A be Subset of T; :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or (f " ) .: A is open )
assume A is open ; :: thesis: (f " ) .: A is open
then f " A is open by A2, A4, TOPS_2:55;
hence (f " ) .: A is open by A1, A3, FUNCT_1:155; :: thesis: verum

end;

assume A5: f " is open ; :: thesis: f is continuous

now

let A be Subset of T; :: thesis: ( A is open implies f " A is open )
assume A is open ; :: thesis: f " A is open
then (f " ) .: A is open by A5, T_0TOPSP:def 2;
hence f " A is open by A1, A3, FUNCT_1:155; :: thesis: verum

end;

hence f is continuous by A2, TOPS_2:55; :: thesis: verum