let seq1, seq2 be without+infty ExtREAL_sequence; :: thesis: ( ( seq1 is convergent_to_+infty & seq2 is convergent_to_+infty implies ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty ) ) & ( seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_-infty implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -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 & lim (seq1 + seq2) = (lim seq1) + (lim seq2) ) ) )
reconsider f1 = - seq1, f2 = - seq2 as without-infty ExtREAL_sequence ;

hereby :: thesis: ( ( seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_-infty implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -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 & lim (seq1 + seq2) = (lim seq1) + (lim seq2) ) ) )

assume ( seq1 is convergent_to_+infty & seq2 is convergent_to_+infty ) ; :: thesis: ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty )
then A2: ( f1 is convergent_to_-infty & f2 is convergent_to_-infty ) by Th17;
then reconsider F = f1 + f2 as convergent ExtREAL_sequence by Th21;
A3: ( f1 + f2 is convergent_to_-infty & f1 + f2 is convergent & lim (f1 + f2) = -infty ) by A2, Th21;
f1 + f2 = f1 - seq2 by Th10
.= - (seq1 + seq2) by Th9 ;
then seq1 + seq2 = - F by Th2;
hence ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty ) by A3, Th17, XXREAL_3:5; :: thesis: verum

end;

hereby :: thesis: ( ( seq1 is convergent_to_-infty & seq2 is convergent_to_-infty implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty ) ) & ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -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 & lim (seq1 + seq2) = (lim seq1) + (lim seq2) ) ) )

assume ( seq1 is convergent_to_+infty & seq2 is convergent_to_finite_number ) ; :: thesis: ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty )
then A2: ( f1 is convergent_to_-infty & f2 is convergent_to_finite_number ) by Th17;
then reconsider F = f1 + f2 as convergent ExtREAL_sequence by Th22;
A3: ( f1 + f2 is convergent_to_-infty & f1 + f2 is convergent & lim (f1 + f2) = -infty ) by A2, Th22;
f1 + f2 = f1 - seq2 by Th10
.= - (seq1 + seq2) by Th9 ;
then seq1 + seq2 = - F by Th2;
hence ( seq1 + seq2 is convergent_to_+infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty ) by A3, Th17, XXREAL_3:5; :: thesis: verum

end;

hereby :: thesis: ( ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -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 & lim (seq1 + seq2) = (lim seq1) + (lim seq2) ) ) )

assume ( seq1 is convergent_to_-infty & seq2 is convergent_to_-infty ) ; :: thesis: ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty )
then A2: ( f1 is convergent_to_+infty & f2 is convergent_to_+infty ) by Th17;
then reconsider F = f1 + f2 as convergent ExtREAL_sequence by Th18;
A3: ( f1 + f2 is convergent_to_+infty & f1 + f2 is convergent & lim (f1 + f2) = +infty ) by A2, Th18;
f1 + f2 = f1 - seq2 by Th10
.= - (seq1 + seq2) by Th9 ;
then seq1 + seq2 = - F by Th2;
hence ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty ) by A3, Th17, XXREAL_3:6; :: thesis: verum

end;

hereby :: thesis: ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number implies ( seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) ) )

assume ( seq1 is convergent_to_-infty & seq2 is convergent_to_finite_number ) ; :: thesis: ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty )
then A2: ( f1 is convergent_to_+infty & f2 is convergent_to_finite_number ) by Th17;
then reconsider F = f1 + f2 as convergent ExtREAL_sequence by Th19;
A3: ( f1 + f2 is convergent_to_+infty & f1 + f2 is convergent & lim (f1 + f2) = +infty ) by A2, Th19;
f1 + f2 = f1 - seq2 by Th10
.= - (seq1 + seq2) by Th9 ;
then seq1 + seq2 = - F by Th2;
hence ( seq1 + seq2 is convergent_to_-infty & seq1 + seq2 is convergent & lim (seq1 + seq2) = -infty ) by A3, Th17, XXREAL_3:6; :: thesis: verum

end;

hereby :: thesis: verum

assume ( seq1 is convergent_to_finite_number & seq2 is convergent_to_finite_number ) ; :: thesis: ( seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) )
then A2: ( f1 is convergent_to_finite_number & f2 is convergent_to_finite_number ) by Th17;
then reconsider F = f1 + f2 as convergent ExtREAL_sequence by Th23;
A3: ( f1 + f2 is convergent_to_finite_number & f1 + f2 is convergent & lim (f1 + f2) = (lim f1) + (lim f2) ) by A2, Th23;
f1 + f2 = f1 - seq2 by Th10
.= - (seq1 + seq2) by Th9 ;
then A4: seq1 + seq2 = - F by Th2;
then A5: lim (seq1 + seq2) = - ((lim f1) + (lim f2)) by A3, Th17;
( seq1 = - f1 & seq2 = - f2 ) by Th2;
then ( lim seq1 = - (lim f1) & lim seq2 = - (lim f2) ) by A2, Th17;
hence ( seq1 + seq2 is convergent_to_finite_number & seq1 + seq2 is convergent & lim (seq1 + seq2) = (lim seq1) + (lim seq2) ) by A3, A4, A5, Th17, XXREAL_3:9; :: thesis: verum

end;