for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Nat st
for n being Nat st n >= m holds
Rseq . n >= 1 holds
not seq is summable