theorem :: DBLSEQ_3:37

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