let Rseq be Function of [:NAT,NAT:],REAL; ( Rseq is P-convergent implies P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) )
assume A1:
Rseq is P-convergent
; P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
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)) - (P-lim Rseq)).| < 1 / m
hence
P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
by Th58; verum