let X be ComplexUnitarySpace; 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; ( 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
; seq1 is Cauchy
consider Nseq being increasing sequence of NAT such that
A3:
seq1 = seq * Nseq
by A2, VALUED_0:def 17;
now 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)) < rlet r be
Real;
( 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
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < rthen 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;
for n, m being Nat st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < rlet n,
m be
Nat;
( n >= k & m >= k implies dist ((seq1 . n),(seq1 . m)) < r )assume that A5:
n >= k
and A6:
m >= k
;
dist ((seq1 . n),(seq1 . m)) < rA7:
(
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;
verum end;
hence
seq1 is Cauchy
; verum