for seq being Complex_Sequence st ex n being Nat st seq ^\ n is summable holds
seq is summable