for D, E being non empty set
for d being Element of D
for h being Function of D,E
for p being FinSequence of D holds h * ([#] (p,d)) = [#] ((h * p),(h . d))