theorem :: CLVECT_2:60

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 - seq2 is Cauchy