theorem :: MOEBIUS2:25

for f being nonnegative-yielding Real_Sequence st f is summable holds
for p being Real st p > 0 holds
ex i being Element of NAT st Sum (f ^\ i) < p