for s being Real_Sequence st ex n being Nat st s ^\ n is summable holds
s is summable