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

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

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

assume
lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {}
; :: thesis: 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

end;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

hence
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)) - 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;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

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

hence
Rseq is P-convergent
; :: thesis: verum
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

end;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;

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - p).| < e ; :: thesis: verum

end;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).| < eend;

hence
ex N being Nat st for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - p).| < eend;

for n, m being Nat st n >= N & m >= N holds

|.((Rseq . (n,m)) - p).| < e ; :: thesis: verum