for seq being Complex_Sequence st ( for n being Nat holds seq . n = 0c ) holds
( seq is summable & Sum seq = 0c )