let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is P-convergent iff lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} )

hereby :: thesis: ( lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} implies Rseq is P-convergent )

assume Rseq is P-convergent ; :: thesis: lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {}
then consider x being Real such that
A1: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - x).| < e ;
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)) - x).| < 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)) - x).| < 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)) - x).| < 1 / m by A1; :: thesis: verum

end;

hence lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} by Th58; :: thesis: verum

end;

assume lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} ; :: thesis: Rseq is P-convergent
then consider p being object such that
A2: p in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by XBOOLE_0:def 1;
reconsider p = p as Real by A2;
ex p0 being Real st
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p0).| < e

proof

take p ; :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < e

hereby :: thesis: verum

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < e
then ex m being Nat st
( not m is zero & 1 / m < e ) by Th5;
then consider m0 being non zero Nat such that
not m0 is zero and
A3: 1 / m0 < e ;
consider n0 being Nat such that
A4: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
|.((Rseq . (n1,n2)) - p).| < 1 / m0 by Th58, A2;

now :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < e

take N = n0; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < e

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.((Rseq . (n,m)) - p).| < e )
assume ( n >= N & m >= N ) ; :: thesis: |.((Rseq . (n,m)) - p).| < e
then |.((Rseq . (n,m)) - p).| < 1 / m0 by A4;
hence |.((Rseq . (n,m)) - p).| < e by A3, XXREAL_0:2; :: thesis: verum

end;

end;

hence ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - p).| < e ; :: thesis: verum

end;

end;

hence Rseq is P-convergent ; :: thesis: verum