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 that
A1: g in product (doms f) and
A2: x in dom g ; :: thesis: (Frege f) .. (g,x) = f .. (x,(g . x))
A3: dom g = dom (doms f) by A1, CARD_3:18;
A4: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
consider h being Function such that
A5: (Frege f) . g = h and
A6: dom h = f " (SubFuncs (rng f)) and
A7: for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) by A1, Def7;
dom (Frege f) = product (doms f) by Def7;
hence (Frege f) .. (g,x) = h . x by A1, A2, A5, A6, A3, A4, FUNCT_5:45
.= f .. (x,(g . x)) by A2, A6, A7, A3, A4 ;
:: thesis: verum