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