let seq1, seq2 be ExtREAL_sequence; :: thesis:
assume that
A1: seq2 is subsequence of seq1 and
A2: seq1 is convergent_to_finite_number ; :: thesis:
( not seq1 is convergent_to_+infty & not seq1 is convergent_to_-infty ) by A2, MESFUNC5:50, MESFUNC5:51;
then consider g being Real such that
B3: ( lim seq1 = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq1)).| < p ) & seq1 is convergent_to_finite_number ) by A2, MESFUNC5:def 12;
reconsider LIM2 = lim seq1 as R_eal ;
ex g being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - g).| < p

take g ; :: thesis:

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider n1 being Nat such that
A4: for m being Nat st n1 <= m holds
|.((seq1 . m) - g).| < p by B3;
take n = n1; :: thesis:
let m be Nat; :: thesis:
assume A5: n <= m ; :: thesis:
consider Nseq being increasing sequence of NAT such that
A6: seq2 = seq1 * Nseq by A1, VALUED_0:def 17;
m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A5, XXREAL_0:2;
seq2 . m = seq1 . (Nseq . m) by A6, FUNCT_2:15, ORDINAL1:def 12;
hence |.((seq2 . m) - g).| < p by A4, A7; :: thesis:

end;

hence A8: seq2 is convergent_to_finite_number by MESFUNC5:def 8; :: thesis:
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - LIM2).| < p

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider n1 being Nat such that
A10: for m being Nat st n1 <= m holds
|.((seq1 . m) - (lim seq1)).| < p by B3;
take n = n1; :: thesis:
let m be Nat; :: thesis:
assume A11: n <= m ; :: thesis:
consider Nseq being increasing sequence of NAT such that
A12: seq2 = seq1 * Nseq by A1, VALUED_0:def 17;
m <= Nseq . m by SEQM_3:14;
then A13: n <= Nseq . m by A11, XXREAL_0:2;
seq2 . m = seq1 . (Nseq . m) by A12, FUNCT_2:15, ORDINAL1:def 12;
hence |.((seq2 . m) - LIM2).| < p by A10, A13; :: thesis:

end;