theorem Th62: :: CARDFIL4:75

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