theorem Th5: :: INT_5:5

for n being Nat
for f, f1, f2 being FinSequence of REAL st len f = n + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds
f . d = (f1 . d) - (f2 . d) ) holds
ex fr being FinSequence of REAL st
( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds
fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (n + 1))) - (f2 . 1) )