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 g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
seq2 . m <= g

let g be Real; :: thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
seq2 . m <= g )
assume g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq2 . m <= g
then consider n1 being Nat such that
A4: for m being Nat st n1 <= m holds
seq1 . m <= g by A2, MESFUNC5:def 10;
take n = n1; :: thesis: for m being Nat st n <= m holds
seq2 . m <= g
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 seq2 . m <= g )
assume A6: n <= m ; :: thesis: seq2 . m <= g
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 seq2 . m <= g by A4, A7; :: thesis: verum

end;

hence seq2 is convergent_to_-infty by MESFUNC5:def 10; :: thesis: lim seq2 = -infty
hence lim seq2 = -infty by MESFUNC5:def 12; :: thesis: verum