let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is P-convergent implies {(P-lim Rseq)} = lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) )
assume Rseq is P-convergent ; :: thesis: {(P-lim Rseq)} = lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
then A1: P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by Th60;
then ex x being Real st lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = {x} by Th59;
hence {(P-lim Rseq)} = lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by A1, TARSKI:def 1; :: thesis: verum