theorem Th13: :: CLOPBAN3:13

for X being ComplexNormSpace
for seq being sequence of X st ( for n being Nat holds seq . n = 0. X ) holds
seq is norm_summable