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) )
A2: f in product (doms F) by A1;
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 A3: 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) )
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; :: thesis: ( ((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; :: 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 A3, A4, FUNCT_1:def 3; :: thesis: verum