let seq1 be subsequence of seq; :: thesis: seq1 is convergent
consider g1 being Point of X such that
A1: 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 BHSP_2:9;
consider Nseq being increasing sequence of NAT such that
A2: seq1 = seq * Nseq by VALUED_0:def 17;

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
A3: for n being Nat st n >= m1 holds
||.((seq . n) - g1).|| < r by A1;
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 A4: n >= m ; :: thesis: ||.((seq1 . n) - g1).|| < r
A5: n in NAT by ORDINAL1:def 12;
Nseq . n >= n by SEQM_3:14;
then A6: Nseq . n >= m by A4, XXREAL_0:2;
seq1 . n = seq . (Nseq . n) by A2, FUNCT_2:15, A5;
hence ||.((seq1 . n) - g1).|| < r by A3, A6; :: thesis: verum

end;

hence seq1 is convergent by BHSP_2:9; :: thesis: verum