theorem Th18: :: LIOUVIL1:18

for f being Real_Sequence
for n being Nat st f . 0 = 0 holds
Sum (FinSeq (f,n)) = Sum (f |_ (Seg n))