let x be set ; :: thesis: for f, g, h, h9 being 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, g, h, h9 be 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 f " (SubFuncs (rng f)) by A1, Th28;
A5: dom (doms f) = f " (SubFuncs (rng f)) by Def2;
( ex f2 being Function st
( h = f2 & dom f2 = dom (doms f) & ( for x being set st x in dom (doms f) holds
f2 . x in (doms f) . x ) ) & (doms f) . x = dom g ) by A1, A2, Th31, 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 = f " (SubFuncs (rng f)) & ( for x being set st x in dom f1 holds
f1 . x = (uncurry f) . (x,(h . x)) ) ) by A2, Def7;
hence h9 . x = (uncurry f) . (x,(h . x)) by A3, A4
.= g . (h . x) by A1, A6, FUNCT_5:45 ;
:: thesis: h9 in product (rngs f)
A7: rng (Frege f) c= product (rngs f) by Lm2;
dom (Frege f) = product (doms f) by Def7;
then h9 in rng (Frege f) by A2, A3, FUNCT_1:def 5;
hence h9 in product (rngs f) by A7; :: thesis: verum