let NTX, NTY be NTopSpace; :: thesis:
let x be Point of NTX; :: thesis:
let y be Point of NTY; :: thesis:
let f be Function of NTX,NTY; :: thesis:
assume that
A1: y = f . x and
A2: for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ; :: thesis:

now :: thesis:

let F be Filter of the carrier of NTX; :: thesis:
assume x in lim_filter F ; :: thesis:
then consider x9 being Point of NTX such that
A3: x = x9 and
A4: F is_filter-finer_than U_FMT x9 ;
A5: U_FMT x c= F by A3, A4, CARDFIL2:def 6;

now :: thesis:

let o be object ; :: thesis:
assume o in U_FMT y ; :: thesis:
then reconsider V = o as Element of U_FMT y ;
consider W being Element of U_FMT x such that
A6: f .: W c= V by A2;
A7: W in F by A5;
reconsider M = f .: W as Subset of NTY ;
A8: W c= f " M by FUNCT_2:42;
f " M c= f " V by A6, RELAT_1:143;
then W c= f " V by A8;
then f " V in F by A7, CARD_FIL:def 1;
then V in { M where M is Subset of NTY : f " M in F } ;
hence o in filter_image (f,F) by CARDFIL2:def 13; :: thesis:

end;

then U_FMT y c= filter_image (f,F) ;
then filter_image (f,F) is_filter-finer_than U_FMT y by CARDFIL2:def 6;
hence y in lim_filter (f,F) ; :: thesis:

end;

hence f is_continuous_at x by A1; :: thesis: