theorem :: WAYBEL_5:7

for F being Function-yielding Function
for f being set st f in dom (Frege F) holds
f is Function ;