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