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