for r being Real
for s being Real_Sequence st r > 0 & ex m being Nat st
for n being Nat st n >= m holds
|.(s . n).| >= r & s is convergent holds
lim s <> 0