theorem :: CARDFIL2:85

for T being non empty TopSpace
for s being sequence of T holds lim_filter (s,(Frechet_Filter NAT)) = lim_f s ;