for f being Real_Sequence
for N, M being Element of NAT holds (Sum (f,N,M)) + (f . (N + 1)) = Sum (f,(N + 1),M) by Lm15;