let x be object ; :: thesis: for g being Function
for f being Function-yielding Function st g in product (doms f) & x in dom g holds
(Frege f) .. (g,x) = f .. (x,(g . x))
let g be Function; :: thesis: for f being Function-yielding Function st g in product (doms f) & x in dom g holds
(Frege f) .. (g,x) = f .. (x,(g . x))
let f be Function-yielding 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:9;
A4: dom (doms f) = dom f by Def1;
consider h being Function such that
A5: (Frege f) . g = h and
A6: dom h = dom f and
A7: for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) by A1, Def6;
dom (Frege f) = product (doms f) by Def6;
hence (Frege f) .. (g,x) = h . x by A1, A2, A5, A6, A3, A4, FUNCT_5:38
.= f .. (x,(g . x)) by A2, A6, A7, A3, A4 ;
:: thesis: verum