theorem :: FUNCT_6:37

for x being object
for g, h, h9 being Function
for f being Function-yielding Function st x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h holds
( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) )