theorem Th36: :: DBLSEQ_3:36

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