let seq1 be subsequence of seq; :: thesis: seq1 is Cauchy
consider Nseq being increasing sequence of NAT such that
A1: seq1 = seq * Nseq by VALUED_0:def 17;

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

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

end;

hence seq1 is Cauchy ; :: thesis: verum