let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent implies ( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 ) )
assume that
A1: Rseq is nonnegative-yielding and
A2: Partial_Sums Rseq is P-convergent ; :: thesis: ( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 )
( Partial_Sums_in_cod1 Rseq is convergent_in_cod1 & Partial_Sums_in_cod2 Rseq is convergent_in_cod2 ) by A1, A2, th1006;
hence ( Partial_Sums Rseq is convergent_in_cod1 & Partial_Sums Rseq is convergent_in_cod2 ) by th01a, th01b; :: thesis: verum