theorem Th12: :: SERIES_1:12
for s being Real_Sequence st s is summable holds
for n being Nat holds s ^\ n is summable