for F being Function-yielding Function
for f being Function st f in dom (Frege F) holds
( dom f = dom F & dom F = dom ((Frege F) . f) )