theorem Th9: :: RFUNCT_2:9

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