theorem :: CLVECT_3:32

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