theorem Th17: :: DBLSEQ_3:17

for seq being convergent ExtREAL_sequence holds
( ( seq is convergent_to_finite_number implies - seq is convergent_to_finite_number ) & ( - seq is convergent_to_finite_number implies seq is convergent_to_finite_number ) & ( seq is convergent_to_+infty implies - seq is convergent_to_-infty ) & ( - seq is convergent_to_-infty implies seq is convergent_to_+infty ) & ( seq is convergent_to_-infty implies - seq is convergent_to_+infty ) & ( - seq is convergent_to_+infty implies seq is convergent_to_-infty ) & - seq is convergent & lim (- seq) = - (lim seq) )