theorem :: LOPBAN_3:33

for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds
( seq is norm_summable iff rseq1 is summable )