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