for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X holds
( ( F # x is convergent_to_+infty implies (- F) # x is convergent_to_-infty ) & ( (- F) # x is convergent_to_-infty implies F # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies (- F) # x is convergent_to_+infty ) & ( (- F) # x is convergent_to_+infty implies F # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )