theorem :: RFUNCT_2:11

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 is non-zero