let f1, f2 be Function; :: thesis:
assume that
A5: dom f1 = product (doms f) and
A6: for g being Function st g in product (doms f) holds
ex h being Function st
( f1 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) and
A7: dom f2 = product (doms f) and
A8: for g being Function st g in product (doms f) holds
ex h being Function st
( f2 . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) ; :: thesis:

let x be set ; :: thesis:
assume A9: x in product (doms f) ; :: thesis:
then consider g being Function such that
A10: x = g and
dom g = dom (doms f) and
for x being set st x in dom (doms f) holds
g . x in (doms f) . x by CARD_3:def 5;
consider h2 being Function such that
A11: f2 . g = h2 and
A12: dom h2 = f " (SubFuncs (rng f)) and
A13: for y being set st y in dom h2 holds
h2 . y = (uncurry f) . (y,(g . y)) by A8, A9, A10;
consider h1 being Function such that
A14: f1 . g = h1 and
A15: dom h1 = f " (SubFuncs (rng f)) and
A16: for y being set st y in dom h1 holds
h1 . y = (uncurry f) . (y,(g . y)) by A6, A9, A10;

end;

end;