let x be set ; :: thesis: for g, f being Function st g in product (doms f) & x in dom g holds
(Frege f) .. g,x = f .. x,(g . x)
let g, f be Function; :: thesis: ( g in product (doms f) & x in dom g implies (Frege f) .. g,x = f .. x,(g . x) )
assume A1: ( g in product (doms f) & x in dom g ) ; :: thesis: (Frege f) .. g,x = f .. x,(g . x)
then consider h being Function such that
A2: ( (Frege f) . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . x,(g . x) ) ) by Def7;
A3: ( dom g = dom (doms f) & dom (doms f) = f " (SubFuncs (rng f)) & dom (Frege f) = product (doms f) ) by A1, Def2, Def7, CARD_3:18;
hence (Frege f) .. g,x = h . x by A1, A2, FUNCT_5:45
.= f .. x,(g . x) by A1, A2, A3 ;
:: thesis: verum