let seq, seq1 be Real_Sequence; :: thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; :: thesis: lim seq1 = lim seq
consider Nseq being V45() sequence of NAT such that
A3: seq1 = seq * Nseq by A1, VALUED_0:def 17;
A4: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < p by A2, SEQ_2:def 7;
take n = n1; :: thesis: for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A6: n <= m ; :: thesis: |.((seq1 . m) - (lim seq)).| < p
m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A6, XXREAL_0:2;
m in NAT by ORDINAL1:def 12;
then seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15;
hence |.((seq1 . m) - (lim seq)).| < p by A5, A7; :: thesis: verum
end;
seq1 is convergent by A1, A2, Th16;
hence lim seq1 = lim seq by A4, SEQ_2:def 7; :: thesis: verum