theorem Th31: :: SERIES_1:31

for s, s1 being Real_Sequence st s is non-increasing & ( for n being Nat holds
( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ) holds
( s is summable iff s1 is summable )