theorem Th28: :: SERIES_1:28

for s, s1 being Real_Sequence st ( for n being Nat holds
( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 holds
s is summable