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

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

hence
P-lim Rseq in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
by Th58; :: thesis: verum
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;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