theorem Th58: :: CARDFIL4:71

for r being Real
for Rseq being Function of [:NAT,NAT:],REAL holds
( r in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m )