theorem Th9: :: WAYBEL_5:9

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