let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: 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; :: thesis: ( Rseq is P-convergent implies ( Rseq1 is P-convergent & P-lim Rseq1 = P-lim Rseq ) )
assume a1: Rseq is P-convergent ; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e
hereby :: thesis: verum
let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e )
assume a4: ( n >= N & m >= N ) ; :: thesis: |.((Rseq1 . (n,m)) - (P-lim Rseq)).| < e
consider 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; :: thesis: verum
end;
end;
hence Rseq1 is P-convergent ; :: thesis: P-lim Rseq1 = P-lim Rseq
hence P-lim Rseq1 = P-lim Rseq by a2, def6; :: thesis: verum