let Rseq, Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; ( Rseq1 is P-convergent & Rseq2 is P-convergent & P-lim Rseq1 = P-lim Rseq2 & ( for n, m being Nat holds
( Rseq1 . (n,m) <= Rseq . (n,m) & Rseq . (n,m) <= Rseq2 . (n,m) ) ) implies ( Rseq is P-convergent & P-lim Rseq = P-lim Rseq1 ) )
assume that
a1:
( Rseq1 is P-convergent & Rseq2 is P-convergent )
and
a2:
P-lim Rseq1 = P-lim Rseq2
and
a3:
for n, m being Nat holds
( Rseq1 . (n,m) <= Rseq . (n,m) & Rseq . (n,m) <= Rseq2 . (n,m) )
; ( Rseq is P-convergent & P-lim Rseq = P-lim Rseq1 )
a4:
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-lim Rseq1)).| < 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
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < e )
assume a5:
0 < e
;
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < e
then consider N1 being
Nat such that a6:
for
n,
m being
Nat st
n >= N1 &
m >= N1 holds
|.((Rseq1 . (n,m)) - (P-lim Rseq1)).| < e
by a1, def6;
consider N2 being
Nat such that a7:
for
n,
m being
Nat st
n >= N2 &
m >= N2 holds
|.((Rseq2 . (n,m)) - (P-lim Rseq1)).| < e
by a1, a2, a5, def6;
reconsider N =
max (
N1,
N2) as
Nat by TARSKI:1;
take
N
;
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < e
a8:
(
max (
N1,
N2)
>= N1 &
max (
N1,
N2)
>= N2 )
by XXREAL_0:25;
hereby verum
let n,
m be
Nat;
( n >= N & m >= N implies |.((Rseq . (n,m)) - (P-lim Rseq1)).| < e )assume
(
n >= N &
m >= N )
;
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < ethen
(
n >= N1 &
m >= N1 &
n >= N2 &
m >= N2 )
by a8, XXREAL_0:2;
then a9:
(
|.((Rseq1 . (n,m)) - (P-lim Rseq1)).| < e &
|.((Rseq2 . (n,m)) - (P-lim Rseq1)).| < e )
by a6, a7;
then a10:
- e < - |.((Rseq1 . (n,m)) - (P-lim Rseq1)).|
by XREAL_1:24;
- |.((Rseq1 . (n,m)) - (P-lim Rseq1)).| <= (Rseq1 . (n,m)) - (P-lim Rseq1)
by ABSVALUE:4;
then a11:
- e < (Rseq1 . (n,m)) - (P-lim Rseq1)
by a10, XXREAL_0:2;
(Rseq2 . (n,m)) - (P-lim Rseq1) <= |.((Rseq2 . (n,m)) - (P-lim Rseq1)).|
by ABSVALUE:4;
then a12:
(Rseq2 . (n,m)) - (P-lim Rseq1) < e
by a9, XXREAL_0:2;
a13:
(
(Rseq1 . (n,m)) - (P-lim Rseq1) <= (Rseq . (n,m)) - (P-lim Rseq1) &
(Rseq . (n,m)) - (P-lim Rseq1) <= (Rseq2 . (n,m)) - (P-lim Rseq1) )
by a3, XREAL_1:9;
then
(
- e < (Rseq . (n,m)) - (P-lim Rseq1) &
(Rseq . (n,m)) - (P-lim Rseq1) < e )
by a11, a12, XXREAL_0:2;
then a14:
|.((Rseq . (n,m)) - (P-lim Rseq1)).| <= e
by ABSVALUE:5;
- ((Rseq . (n,m)) - (P-lim Rseq1)) <> e
by a3, a11, XREAL_1:9;
then
|.((Rseq . (n,m)) - (P-lim Rseq1)).| <> e
by a13, a12, ABSVALUE:1;
hence
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < e
by a14, XXREAL_0:1;
verum
end;
end;
hence
Rseq is P-convergent
; P-lim Rseq = P-lim Rseq1
hence
P-lim Rseq = P-lim Rseq1
by a4, def6; verum