let Rseq be Function of [:NAT,NAT:],REAL; ( Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent implies ( P-lim (Partial_Sums Rseq) = Sum (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) & P-lim (Partial_Sums Rseq) = Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) ) )
assume that
A1:
Rseq is nonnegative-yielding
and
A2:
Partial_Sums Rseq is P-convergent
; ( P-lim (Partial_Sums Rseq) = Sum (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) & P-lim (Partial_Sums Rseq) = Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) )
A4:
( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 )
by A1, A2, th1006a;
A5:
Sum (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) = lim (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)))
by SERIES_1:def 3;
for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 (Partial_Sums Rseq)) . m) - (cod1_major_iterated_lim (Partial_Sums Rseq))).| < e
by A2, A4, DBLSEQ_1:def 7;
then cod1_major_iterated_lim (Partial_Sums Rseq) =
lim (lim_in_cod1 (Partial_Sums Rseq))
by A2, A4, SEQ_2:def 7
.=
Sum (lim_in_cod1 (Partial_Sums_in_cod1 Rseq))
by A5, A1, A2, th1006a, th03a
;
hence
P-lim (Partial_Sums Rseq) = Sum (lim_in_cod1 (Partial_Sums_in_cod1 Rseq))
by A1, A2, th1006a, DBLSEQ_1:4; P-lim (Partial_Sums Rseq) = Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq))
A6:
Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) = lim (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)))
by SERIES_1:def 3;
for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod2 (Partial_Sums Rseq)) . m) - (cod2_major_iterated_lim (Partial_Sums Rseq))).| < e
by A2, A4, DBLSEQ_1:def 8;
then cod2_major_iterated_lim (Partial_Sums Rseq) =
lim (lim_in_cod2 (Partial_Sums Rseq))
by A2, A4, SEQ_2:def 7
.=
Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq))
by A6, A1, A2, th1006a, th03b
;
hence
P-lim (Partial_Sums Rseq) = Sum (lim_in_cod2 (Partial_Sums_in_cod2 Rseq))
by A1, A2, th1006a, DBLSEQ_1:3; verum