theorem :: RFUNCT_2:12

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 ^) holds
(h ^) /* seq = (h /* seq) "