theorem :: COMSEQ_3:59

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