theorem :: FINTOPO8:17

for NTX, NTY being NTopSpace
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st y = f . x & ( for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ) holds
f is_continuous_at x by Lm25;