theorem Th36: :: MOEBIUS3:7

for f being summable Real_Sequence
for n being Nat st f is positive-yielding holds
Sum (f ^\ (n + 1)) > 0