let X be RealUnitarySpace; :: thesis: for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
let seq, seq1 be sequence of X; :: 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 increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A1, VALUED_0:def 17;

A4: now :: thesis: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),(lim seq)) < r

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),(lim seq)) < r )
assume r > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),(lim seq)) < r
then consider m1 being Nat such that
A5: for n being Nat st n >= m1 holds
dist ((seq . n),(lim seq)) < r by A2, BHSP_2:def 2;
take m = m1; :: thesis: for n being Nat st n >= m holds
dist ((seq1 . n),(lim seq)) < r
let n be Nat; :: thesis: ( n >= m implies dist ((seq1 . n),(lim seq)) < r )
assume A6: n >= m ; :: thesis: dist ((seq1 . n),(lim seq)) < r
A7: n in NAT by ORDINAL1:def 12;
Nseq . n >= n by SEQM_3:14;
then A8: Nseq . n >= m by A6, XXREAL_0:2;
seq1 . n = seq . (Nseq . n) by A3, FUNCT_2:15, A7;
hence dist ((seq1 . n),(lim seq)) < r by A5, A8; :: thesis: verum

end;

seq1 is convergent by A1, A2;
hence lim seq1 = lim seq by A4, BHSP_2:def 2; :: thesis: verum