for i being Nat
for f being FinSequence of COMPLEX holds f = ((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1))