theorem Th26: :: PDIFF_7:26

for n being non zero Nat
for h, g being FinSequence of REAL n st len h = (len g) + 1 & ( for i being Nat st i in dom g holds
g /. i = (h /. i) - (h /. (i + 1)) ) holds
(h /. 1) - (h /. (len h)) = Sum g