theorem Th85: :: CLVECT_2:85

for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds
seq1 is Cauchy