for K being Nat
for seq being Real_Sequence st seq is summable & ( for k being Nat holds seq . k >= 0 ) holds
Sum seq >= (Partial_Sums seq) . K