:: deftheorem defines lim_filter CARDFIL2:def 26 :
for X being non empty set
for T being non empty TopSpace
for f being Function of X, the carrier of T
for F being Filter of X holds lim_filter (f,F) = lim_filter (filter_image (f,F));