for r being Real
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st h is total holds
(r (#) h) /* seq = r (#) (h /* seq)