for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 + seq2 is convergent