let F be Function-yielding Function; :: thesis: for f being Function st f in dom (Frege F) holds
( dom f = dom F & dom F = dom ((Frege F) . f) )
let f be Function; :: thesis: ( f in dom (Frege F) implies ( dom f = dom F & dom F = dom ((Frege F) . f) ) )
assume f in dom (Frege F) ; :: thesis: ( dom f = dom F & dom F = dom ((Frege F) . f) )
then A1: f in product (doms F) ;
then ex g being Function st
( g = f & dom g = dom (doms F) & ( for x being object st x in dom (doms F) holds
g . x in (doms F) . x ) ) by CARD_3:def 5;
hence A2: dom f = dom F by FUNCT_6:59; :: thesis: dom F = dom ((Frege F) . f)
thus dom ((Frege F) . f) = dom (F .. f) by A1, PRALG_2:def 2
.= (dom F) /\ (dom f) by PRALG_1:def 19
.= dom F by A2 ; :: thesis: verum