for seq being Complex_Sequence st seq is absolutely_summable holds
seq is summable