theorem :: CLVECT_2:26

for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 )