theorem :: CLOPBAN3:36

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