theorem SumMono: :: PRIMRECI:8

for i, j being Nat
for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) & i <= j holds
Sum (s ^\ j) <= Sum (s ^\ i)