theorem Th65: :: DBLSEQ_3:65

for f being nonnegative Function of [:NAT,NAT:],ExtREAL holds
( ( f is convergent_in_cod1 implies lim_in_cod1 f is nonnegative ) & ( f is convergent_in_cod2 implies lim_in_cod2 f is nonnegative ) )