for seq being Complex_Sequence
for x being Nat st ( for k being Nat st k >= x holds
seq . k = 0 ) holds
seq is summable