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 A5: ( n >= k & m >= k ) ; :: thesis: dist (seq1 . n),(seq1 . m) < r
( Nseq . n >= n & Nseq . m >= m ) by SEQM_3:33;
then A6: ( Nseq . n >= k & Nseq . m >= k ) by A5, XXREAL_0:2;
( seq1 . n = seq . (Nseq . n) & seq1 . m = seq . (Nseq . m) ) by A3, FUNCT_2:21;
hence dist (seq1 . n),(seq1 . m) < r by A4, A6; :: thesis: verum

end;

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