let Rseq be Function of [:NAT,NAT:],REAL; for a being Real st ( for n, m being Nat holds Rseq . (n,m) = a ) holds
( Rseq is P-convergent & P-lim Rseq = a )
let a be Real; ( ( for n, m being Nat holds Rseq . (n,m) = a ) implies ( Rseq is P-convergent & P-lim Rseq = a ) )
assume a1:
for n, m being Nat holds Rseq . (n,m) = a
; ( Rseq is P-convergent & P-lim Rseq = a )
a3:
now 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)) - a).| < elet e be
Real;
( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - a).| < e )assume a2:
0 < e
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - a).| < ereconsider N =
0 as
Nat ;
take N =
N;
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - a).| < ethus
for
n,
m being
Nat st
n >= N &
m >= N holds
|.((Rseq . (n,m)) - a).| < e
by a4;
verum end;
hence
Rseq is P-convergent
; P-lim Rseq = a
hence
P-lim Rseq = a
by a3, def6; verum