theorem :: CLVECT_3:14

for X being ComplexUnitarySpace
for seq being sequence of X st ex k being Nat st seq ^\ k is summable holds
seq is summable