for f being Real_Sequence
for n being Nat st f is summable & f . 0 = 0 holds
Sum f = (Sum (FinSeq (f,n))) + (Sum (f ^\ (n + 1)))