let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum