for seq1 being Real_Sequence st seq1 is summable holds
ex r being Real st
( 0 < r & ( for k being Nat holds |.(Sum (seq1 ^\ k)).| < r ) )