let X be RealUnitarySpace; :: 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

let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r
then consider l being Element of NAT such that
A4: for n, m being Element of NAT st n >= l & m >= l holds
dist ((seq . n),(seq . m)) < r by A1, Def1;
take k = l; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r
let n, m be Element of 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
Nseq . n >= n by SEQM_3:14;
then A7: Nseq . n >= k by A5, XXREAL_0:2;
Nseq . m >= m by SEQM_3:14;
then A8: Nseq . m >= k by A6, XXREAL_0:2;
( seq1 . n = seq . (Nseq . n) & seq1 . m = seq . (Nseq . m) ) by A3, FUNCT_2:15;
hence dist ((seq1 . n),(seq1 . m)) < r by A4, A7, A8; :: thesis: verum

end;

hence seq1 is Cauchy by Def1; :: thesis: verum