let F be Function-yielding Function; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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) )
set G = (Frege F) . f;
let i be set ; :: thesis: ( 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 A2: i in dom F ; :: thesis: ( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) )
A3: f in product (doms F) by A1, PARTFUN1:def 4;
then A4: (Frege F) . f = F .. f by PRALG_2:def 8;
i in dom (doms F) by A2, FUNCT_6:89;
then f . i in (doms F) . i by A3, CARD_3:18;
hence f . i in dom (F . i) by A2, FUNCT_6:31; :: thesis: ( ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) )
thus A5: ((Frege F) . f) . i = (F . i) . (f . i) by A2, A4, PRALG_1:def 17; :: thesis: (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 A2, A5, FUNCT_1:def 5; :: thesis: verum