theorem :: NEWTON04:36

for i being Nat
for f being complex-valued FinSequence holds f = ((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1))