let Rseq be Function of [:NAT,NAT:],REAL; ( Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent implies ( lim_in_cod1 (Partial_Sums_in_cod1 Rseq) is summable & lim_in_cod2 (Partial_Sums_in_cod2 Rseq) is summable ) )
assume that
A1:
Rseq is nonnegative-yielding
and
A2:
Partial_Sums Rseq is P-convergent
; ( lim_in_cod1 (Partial_Sums_in_cod1 Rseq) is summable & lim_in_cod2 (Partial_Sums_in_cod2 Rseq) is summable )
( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 )
by A1, A2, th1006a;
then A3:
( lim_in_cod1 (Partial_Sums Rseq) is convergent & lim_in_cod2 (Partial_Sums Rseq) is convergent )
by A2;
then
Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) is convergent
by A1, A2, th1006a, th03a;
hence
lim_in_cod1 (Partial_Sums_in_cod1 Rseq) is summable
by SERIES_1:def 2; lim_in_cod2 (Partial_Sums_in_cod2 Rseq) is summable
Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) is convergent
by A3, A1, A2, th1006a, th03b;
hence
lim_in_cod2 (Partial_Sums_in_cod2 Rseq) is summable
by SERIES_1:def 2; verum