theorem Th8: :: WAYBEL_5:8

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) )