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

now :: thesis:

let x be Point of NTX; :: thesis:
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:

let V be Element of U_FMT y; :: thesis:
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:

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

now :: thesis:

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

end;

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

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:

now :: thesis:

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

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= O by FUNCT_1:75;
hence f .: (f " O) c= V by A4; :: thesis:

end;

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

end;

hence f is_continuous_at x by Lm25; :: thesis:

end;

hence f is continuous ; :: thesis: