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