for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds filter_image (s,(Frechet_Filter [:NAT,NAT:])) = { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }