theorem :: DBLSEQ_3:66

for f being nonnegative Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums_in_cod1 f is convergent_in_cod1 & Partial_Sums_in_cod2 f is convergent_in_cod2 ) by RINFSUP2:37;