for d being XFinSequence of REAL
for x, i being Nat st i in dom d holds
(d (#) (seq_a^ (x,1,0))) . i = (d . i) * (x to_power i)