let X be ComplexUnitarySpace; :: thesis: for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds
seq1 is convergent
let seq, seq1 be sequence of X; :: thesis: ( seq is convergent & seq1 is subsequence of seq implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is convergent
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def 17;
consider g1 being Point of X such that
A4: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g1).|| < r by A1, Th9;

now :: thesis: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq1 . n) - g1).|| < r

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

end;

hence seq1 is convergent by Th9; :: thesis: verum