theorem :: SERIES_1:30

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
not s is summable