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