for f being complex-valued XFinSequence
for x being Nat holds (f ^ (seq_const 0)) . x = f . x