theorem :: ASYMPT_1:74

for f, g being Real_Sequence
for M, N being Element of NAT st N >= M + 1 & ( for n being Element of NAT st M + 1 <= n & n <= N holds
f . n <= g . n ) holds
Sum (f,N,M) <= Sum (g,N,M) by Lm16;