let seq1, seq2 be ExtREAL_sequence; :: thesis: ( seq2 is subsequence of seq1 & seq1 is convergent_to_finite_number implies ( seq2 is convergent_to_finite_number & lim seq1 = lim seq2 ) )
assume that
A1: seq2 is subsequence of seq1 and
A2: seq1 is convergent_to_finite_number ; :: thesis: ( seq2 is convergent_to_finite_number & lim seq1 = lim seq2 )
( 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

proof

take g ; :: thesis: 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

hereby :: thesis: verum

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - g).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - g).| < p
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: for m being Nat st n <= m holds
|.((seq2 . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq2 . m) - g).| < p )
assume A5: n <= m ; :: thesis: |.((seq2 . m) - g).| < p
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: verum

end;

end;

hence A8: seq2 is convergent_to_finite_number by MESFUNC5:def 8; :: thesis: lim seq1 = lim seq2
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

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - LIM2).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq2 . m) - LIM2).| < p
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: for m being Nat st n <= m holds
|.((seq2 . m) - LIM2).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq2 . m) - LIM2).| < p )
assume A11: n <= m ; :: thesis: |.((seq2 . m) - LIM2).| < p
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: verum

end;

hence lim seq1 = lim seq2 by A8, B3, MESFUNC5:def 12; :: thesis: verum