theorem :: RFUNCT_2:16

for X being set
for W being non empty set
for h being PartFunc of W,REAL
for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds
((h ^) | X) /* seq = ((h | X) /* seq) "