let X be non empty MetrSpace; :: thesis: for S, S1 being sequence of X st S is Cauchy & S1 is subsequence of S holds
S1 is Cauchy
let S, S1 be sequence of X; :: thesis: ( S is Cauchy & S1 is subsequence of S implies S1 is Cauchy )
assume that
A1: S is Cauchy and
A2: S1 is subsequence of S ; :: thesis: S1 is Cauchy
consider Nseq being increasing sequence of NAT such that
A3: S1 = S * Nseq by A2, VALUED_0:def 17;
for r being Real st 0 < r holds
ex m being Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
then consider m1 being Nat such that
A4: for n, k being Nat st m1 <= n & m1 <= k holds
dist ((S . n),(S . k)) < r by A1;
take m = m1; :: thesis: for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r
for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r

proof

let n, k be Nat; :: thesis: ( m <= n & m <= k implies dist ((S1 . n),(S1 . k)) < r )
assume that
A5: m <= n and
A6: m <= k ; :: thesis: dist ((S1 . n),(S1 . k)) < r
k <= Nseq . k by SEQM_3:14;
then A7: m1 <= Nseq . k by A6, XXREAL_0:2;
A8: k in NAT by ORDINAL1:def 12;
A9: n in NAT by ORDINAL1:def 12;
dom S = NAT by FUNCT_2:def 1;
then ( dom Nseq = NAT & Nseq . k in dom S ) by FUNCT_2:def 1;
then k in dom (S * Nseq) by FUNCT_1:11, A8;
then A10: S1 . k = S . (Nseq . k) by A3, FUNCT_1:12;
dom S = NAT by FUNCT_2:def 1;
then ( dom Nseq = NAT & Nseq . n in dom S ) by FUNCT_2:def 1;
then n in dom (S * Nseq) by FUNCT_1:11, A9;
then A11: S1 . n = S . (Nseq . n) by A3, FUNCT_1:12;
n <= Nseq . n by SEQM_3:14;
then m1 <= Nseq . n by A5, XXREAL_0:2;
hence dist ((S1 . n),(S1 . k)) < r by A4, A11, A7, A10; :: thesis: verum

end;

hence for n, k being Nat st m <= n & m <= k holds
dist ((S1 . n),(S1 . k)) < r ; :: thesis: verum

end;

hence S1 is Cauchy ; :: thesis: verum