let seq1, seq2 be ExtREAL_sequence; :: thesis: ( seq2 is subsequence of seq1 & seq1 is convergent_to_+infty implies ( seq2 is convergent_to_+infty & lim seq2 = +infty ) )
assume that
A1: seq2 is subsequence of seq1 and
A2: seq1 is convergent_to_+infty ; :: thesis: ( seq2 is convergent_to_+infty & lim 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 <= seq2 . m
let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= seq2 . m )
assume 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= seq2 . m
then consider n1 being Nat such that
A4: for m being Nat st n1 <= m holds
g <= seq1 . m by A2, MESFUNC5:def 9;
take n = n1; :: thesis: for m being Nat st n <= m holds
g <= seq2 . m
consider Nseq being increasing sequence of NAT such that
A5: seq2 = seq1 * Nseq by A1, VALUED_0:def 17;
let m be Nat; :: thesis: ( n <= m implies g <= seq2 . m )
assume A6: n <= m ; :: thesis: g <= seq2 . m
m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A6, XXREAL_0:2;
seq2 . m = seq1 . (Nseq . m) by A5, FUNCT_2:15, ORDINAL1:def 12;
hence g <= seq2 . m by A4, A7; :: thesis: verum
end;
hence seq2 is convergent_to_+infty by MESFUNC5:def 9; :: thesis: lim seq2 = +infty
hence lim seq2 = +infty by MESFUNC5:def 12; :: thesis: verum