theorem Th13: :: CLVECT_3:13

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