for seq being Complex_Sequence st seq is summable holds
( seq is convergent & lim seq = 0c )