theorem :: LOPBAN_3:35

for X being RealNormSpace
for seq being sequence of X
for p being Real st p <= 1 & ( for n being Nat st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
not seq is norm_summable by SERIES_1:33;