let x be object ; :: thesis: for g, h, h9 being Function
for f being Function-yielding Function st x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h holds
( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) )
let g, h, h9 be Function; :: thesis: for f being Function-yielding Function st x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h holds
( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) )
let f be Function-yielding Function; :: thesis: ( x in dom f & g = f . x & h in product (doms f) & h9 = (Frege f) . h implies ( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) ) )
assume that
A1: ( x in dom f & g = f . x ) and
A2: h in product (doms f) and
A3: h9 = (Frege f) . h ; :: thesis: ( h . x in dom g & h9 . x = g . (h . x) & h9 in product (rngs f) )
A4: x in dom f by A1;
A5: dom (doms f) = dom f by Def1;
( ex f2 being Function st
( h = f2 & dom f2 = dom (doms f) & ( for x being object st x in dom (doms f) holds
f2 . x in (doms f) . x ) ) & (doms f) . x = dom g ) by A1, A2, Th18, CARD_3:def 5;
hence A6: h . x in dom g by A5, A4; :: thesis: ( h9 . x = g . (h . x) & h9 in product (rngs f) )
ex f1 being Function st
( (Frege f) . h = f1 & dom f1 = dom f & ( for x being object st x in dom f1 holds
f1 . x = (uncurry f) . (x,(h . x)) ) ) by A2, Def6;
hence h9 . x = (uncurry f) . (x,(h . x)) by A3, A4
.= g . (h . x) by A1, A6, FUNCT_5:38 ;
:: thesis: h9 in product (rngs f)
A7: rng (Frege f) c= product (rngs f) by Lm1;
dom (Frege f) = product (doms f) by Def6;
then h9 in rng (Frege f) by A2, A3, FUNCT_1:def 3;
hence h9 in product (rngs f) by A7; :: thesis: verum