let Rseq be Function of [:NAT,NAT:],REAL; for Rseq1 being subsequence of Rseq st Rseq is P-convergent holds
( Rseq1 is P-convergent & P-lim Rseq1 = P-lim Rseq )
let Rseq1 be subsequence of Rseq; ( Rseq is P-convergent implies ( Rseq1 is P-convergent & P-lim Rseq1 = P-lim Rseq ) )
assume a1:
Rseq is P-convergent
; ( Rseq1 is P-convergent & P-lim Rseq1 = P-lim Rseq )
a2:
for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e
proof
let e be
Real;
( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e )
assume
0 < e
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e
then consider N being
Nat such that a3:
for
n,
m being
Nat st
n >= N &
m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq)).| < e
by a1, def6;
take
N
;
for n, m being Nat st n >= N & m >= N holds
|.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e
hereby verum
let n,
m be
Nat;
( n >= N & m >= N implies |.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e )assume a4:
(
n >= N &
m >= N )
;
|.((Rseq1 . (n,m)) - (P-lim Rseq)).| < econsider I1,
I2 being
V113()
sequence of
NAT such that a5:
for
n,
m being
Nat holds
Rseq1 . (
n,
m)
= Rseq . (
(I1 . n),
(I2 . m))
by def9;
(
I1 . n >= n &
I2 . m >= m )
by lem01;
then
(
I1 . n >= N &
I2 . m >= N )
by a4, XXREAL_0:2;
then
|.((Rseq . ((I1 . n),(I2 . m))) - (P-lim Rseq)).| < e
by a3;
hence
|.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e
by a5;
verum
end;
end;
hence
Rseq1 is P-convergent
; P-lim Rseq1 = P-lim Rseq
hence
P-lim Rseq1 = P-lim Rseq
by a2, def6; verum