for seq being Complex_Sequence st seq is summable holds
for n being Nat holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))