theorem :: DBLSEQ_3:25

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