theorem :: DBLSEQ_3:31

for f being Function of [:NAT,NAT:],ExtREAL holds
( ( ( f is convergent_in_cod1_to_+infty or f is convergent_in_cod1_to_-infty or f is convergent_in_cod1_to_finite ) implies f is convergent_in_cod1 ) & ( ( f is convergent_in_cod2_to_+infty or f is convergent_in_cod2_to_-infty or f is convergent_in_cod2_to_finite ) implies f is convergent_in_cod2 ) )