for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable