let F be 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) )
let f be Function; ( f in dom (Frege F) implies 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) ) )
assume A1:
f in dom (Frege F)
; 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) )
A2:
f in product (doms F)
by A1;
set G = (Frege F) . f;
let i be set ; ( i in dom F implies ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) ) )
assume A3:
i in dom F
; ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) )
i in dom f
by Th8, A1, A3;
then
i in (dom F) /\ (dom f)
by A3, XBOOLE_0:def 4;
then a3:
i in dom (F .. f)
by PRALG_1:def 19;
i in dom (doms F)
by A3, FUNCT_6:59;
then
f . i in (doms F) . i
by A2, CARD_3:9;
hence
f . i in dom (F . i)
by A3, FUNCT_6:22; ( ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) )
(Frege F) . f = F .. f
by A2, PRALG_2:def 2;
hence A4:
((Frege F) . f) . i = (F . i) . (f . i)
by a3, PRALG_1:def 19; (F . i) . (f . i) in rng ((Frege F) . f)
dom ((Frege F) . f) = dom F
by A1, Th8;
hence
(F . i) . (f . i) in rng ((Frege F) . f)
by A3, A4, FUNCT_1:def 3; verum