let X be ComplexUnitarySpace; :: thesis: for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds
seq1 is Cauchy
let seq, seq1 be sequence of X; :: thesis: ( seq is Cauchy & seq1 is subsequence of seq implies seq1 is Cauchy )
assume that
A1: seq is Cauchy and
A2: seq1 is subsequence of seq ; :: thesis: seq1 is Cauchy
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, 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
A4: for n, m being Nat st n >= l & m >= l holds
dist ((seq . n),(seq . m)) < r by A1;
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
A5: n >= k and
A6: m >= k ; :: thesis: dist ((seq1 . n),(seq1 . m)) < r
A7: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
Nseq . n >= n by SEQM_3:14;
then A8: Nseq . n >= k by A5, XXREAL_0:2;
Nseq . m >= m by SEQM_3:14;
then A9: Nseq . m >= k by A6, XXREAL_0:2;
( seq1 . n = seq . (Nseq . n) & seq1 . m = seq . (Nseq . m) ) by A3, FUNCT_2:15, A7;
hence dist ((seq1 . n),(seq1 . m)) < r by A4, A8, A9; :: thesis: verum

end;

hence seq1 is Cauchy ; :: thesis: verum