let NTX, NTY be NTopSpace; :: thesis: for f being Function of NTX,NTY st ( for S being open Subset of NTY holds f " S is open Subset of NTX ) holds
f is continuous
let f be Function of NTX,NTY; :: thesis: ( ( for S being open Subset of NTY holds f " S is open Subset of NTX ) implies f is continuous )
assume A1: for S being open Subset of NTY holds f " S is open Subset of NTX ; :: thesis: f is continuous

now :: thesis: for x being Point of NTX holds f is_continuous_at x

let x be Point of NTX; :: thesis: f is_continuous_at x
dom f = the carrier of NTX by FUNCT_2:def 1;
then f . x in rng f by FUNCT_1:3;
then reconsider y = f . x as Point of NTY ;

now :: thesis: for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V

let V be Element of U_FMT y; :: thesis: ex W being Element of U_FMT x st f .: W c= V
consider W9 being Element of U_FMT y such that
A2: for z being Element of NTY st z is Element of W9 holds
V is Element of U_FMT z by FINTOPO7:def 4;
reconsider V9 = V as Subset of NTY ;

now :: thesis: ( not W9 is empty & V9 is a_neighborhood of W9 )

thus not W9 is empty by FINTOPO7:def 3; :: thesis: V9 is a_neighborhood of W9

now :: thesis: for x being Element of NTY st x in W9 holds
V9 in U_FMT x

let x be Element of NTY; :: thesis: ( x in W9 implies V9 in U_FMT x )
assume x in W9 ; :: thesis: V9 in U_FMT x
then V is Element of U_FMT x by A2;
hence V9 in U_FMT x ; :: thesis: verum

end;

hence V9 is a_neighborhood of W9 by FINTOPO7:def 6; :: thesis: verum

end;

then consider O being open Subset of NTY such that
A3: W9 c= O and
A4: O c= V9 by FINTOPO7:16;

now :: thesis: ( f " O in U_FMT x & f .: (f " O) c= V )

now :: thesis: ( y in O & x in dom f )

thus y in O by A3, FINTOPO7:def 3; :: thesis: x in dom f
dom f = the carrier of NTX by FUNCT_2:def 1;
hence x in dom f ; :: thesis: verum

end;

then x in f " O by FUNCT_1:def 7;
hence f " O in U_FMT x by A1, FINTOPO7:def 1; :: thesis: f .: (f " O) c= V
f .: (f " O) c= O by FUNCT_1:75;
hence f .: (f " O) c= V by A4; :: thesis: verum

end;

hence ex W being Element of U_FMT x st f .: W c= V ; :: thesis: verum

end;

hence f is_continuous_at x by Lm25; :: thesis: verum

end;

hence f is continuous ; :: thesis: verum