theorem :: FUNCT_6:36

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