theorem Th9: :: CLVECT_3:9

for X being ComplexUnitarySpace
for seq being sequence of X st seq is summable holds
( seq is convergent & lim seq = 0. X )