theorem :: ASYMPT_1:76

for f being Real_Sequence
for b being Real
for N being Element of NAT st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = b ) holds
for M being Element of NAT holds Sum (f,N,M) = b * (N - M) by Lm18;