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 ) )
assume A1: ( 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 )

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 A2: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= (seq1 + seq2) . m
then consider n1 being Nat such that
A3: for m being Nat st n1 <= m holds
g / 2 <= seq1 . m by A1, MESFUNC5:def 9;
consider n2 being Nat such that
A4: for m being Nat st n2 <= m holds
g / 2 <= seq2 . m by A1, A2, MESFUNC5:def 9;
reconsider N1 = n1, N2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max (N1,N2) as Nat ;
A5: ( 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 A5, XXREAL_0:2;
then ( g / 2 <= seq1 . m & g / 2 <= seq2 . m ) by A3, A4;
then A6: (g / 2) + (g / 2) <= (seq1 . m) + (seq2 . m) by XXREAL_3:36;
m is Element of NAT by ORDINAL1:def 12;
hence g <= (seq1 + seq2) . m by A6, 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 A7: 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 A7, MESFUNC5:def 12; :: thesis: verum