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