:: deftheorem defines lim_filter FINTOPO8:def 2 :
for NTX, NTY being non empty strict U_FMT_filter FMT_Space_Str
for f being Function of NTX,NTY
for F being Filter of the carrier of NTX holds lim_filter (f,F) = lim_filter (filter_image (f,F));