let X be ComplexUnitarySpace; :: thesis: for seq1, seq being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
let seq1, seq 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

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

end;

seq1 is convergent by A1, A2, Th88;
hence lim seq1 = lim seq by A4, Def2; :: thesis: verum