theorem Th42: :: NDIFF_5:42

for S being RealNormSpace
for h, g being FinSequence of S 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