let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is P-convergent implies P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) )
assume A1: Rseq is P-convergent ; :: thesis: 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
proof
let m be non zero Nat; :: thesis: ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - (P-lim Rseq)).| < 1 / m
0 / m < 1 / m by XREAL_1:74;
hence ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - (P-lim Rseq)).| < 1 / m by A1, DBLSEQ_1:def 2; :: thesis: verum
end;
hence P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by Th58; :: thesis: verum