let seq1, seq2 be without+infty ExtREAL_sequence; :: 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 ) )
assume A1: ( 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 consider S2 being Real such that
A2: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - S2).| < g by MESFUNC5:def 8;

now :: thesis: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= (seq1 + seq2) . m

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= (seq1 + seq2) . m )
assume A3: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= (seq1 + seq2) . m
set G = max (1,((2 * g) - S2));
A4: ( 1 <= max (1,((2 * g) - S2)) & (2 * g) - S2 <= max (1,((2 * g) - S2)) ) by XXREAL_0:25;
then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
max (1,((2 * g) - S2)) <= seq1 . m by A1, MESFUNC5:def 9;
consider n2 being Nat such that
A6: for m being Nat st n2 <= m holds
|.((seq2 . m) - S2).| < g by A2, A3;
reconsider N1 = n1, N2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max (N1,N2) as Nat ;
A7: ( n1 <= n & n2 <= n ) by XXREAL_0:25;

now :: thesis: for m being Nat st n <= m holds
g <= (seq1 + seq2) . m

let m be Nat; :: thesis: ( n <= m implies g <= (seq1 + seq2) . m )
assume n <= m ; :: thesis: g <= (seq1 + seq2) . m
then ( n1 <= m & n2 <= m ) by A7, XXREAL_0:2;
then A8: ( max (1,((2 * g) - S2)) <= seq1 . m & |.((seq2 . m) - S2).| < g ) by A5, A6;
reconsider g1 = g as R_eal by XXREAL_0:def 1;
- g1 < (seq2 . m) - S2 by A8, EXTREAL1:21;
then (- g1) + S2 < seq2 . m by XXREAL_3:53;
then A9: (max (1,((2 * g) - S2))) + ((- g1) + S2) <= (seq1 . m) + (seq2 . m) by A8, XXREAL_3:36;
- g1 = - g by XXREAL_3:def 3;
then (- g1) + S2 = (- g) + S2 by XXREAL_3:def 2;
then ((2 * g) - S2) + ((- g1) + S2) = ((2 * g) - S2) + ((- g) + S2) by XXREAL_3:def 2;
then g <= (max (1,((2 * g) - S2))) + ((- g1) + S2) by A4, XXREAL_3:36;
then A10: g <= (seq1 . m) + (seq2 . m) by A9, XXREAL_0:2;
m is Element of NAT by ORDINAL1:def 12;
hence g <= (seq1 + seq2) . m by A10, Th7; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
g <= (seq1 + seq2) . m ; :: thesis: verum

end;

hence A11: seq1 + seq2 is convergent_to_+infty by MESFUNC5:def 9; :: thesis: ( seq1 + seq2 is convergent & lim (seq1 + seq2) = +infty )
hence seq1 + seq2 is convergent ; :: thesis: lim (seq1 + seq2) = +infty
thus lim (seq1 + seq2) = +infty by A11, MESFUNC5:def 12; :: thesis: verum