for D being non empty set
for f being FinSequence of D
for d being Element of D
for i being Nat st i in dom f holds
(f +* (i,d)) /. i = d