theorem :: FINTOPO8:15

for NTX, NTY being NTopSpace
for x being Point of NTX
for f being Function of NTX,NTY holds filter_image (f,(U_FMT x)) = { M where M is Subset of NTY : f " M in U_FMT x } by CARDFIL2:def 13;