theorem Th61: :: CARDFIL4:74

for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is P-convergent iff lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} )