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