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