:: deftheorem defines lim_f CARDFIL2:def 27 :
for T being non empty TopSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T holds lim_f f = lim_filter (filter_image (f,(Tails_Filter L)));