let f1, f2 be Function; :: thesis: ( dom f1 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( f1 . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) ) & dom f2 = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( f2 . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) ) implies f1 = f2 )
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 = dom f & ( for x being object 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 = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) ; :: thesis: f1 = f2

now :: thesis: for x being object st x in product (doms f) holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in product (doms f) implies f1 . x = f2 . x )
assume A9: x in product (doms f) ; :: thesis: f1 . x = f2 . x
then consider g being Function such that
A10: x = g and
dom g = dom (doms f) and
for x being object 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 = dom f and
A13: for y being object 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 = dom f and
A16: for y being object st y in dom h1 holds
h1 . y = (uncurry f) . (y,(g . y)) by A6, A9, A10;

now :: thesis: for z being object st z in dom f holds
h1 . z = h2 . z

let z be object ; :: thesis: ( z in dom f implies h1 . z = h2 . z )
assume A17: z in dom f ; :: thesis: h1 . z = h2 . z
then h1 . z = (uncurry f) . (z,(g . z)) by A15, A16;
hence h1 . z = h2 . z by A12, A13, A17; :: thesis: verum

end;

hence f1 . x = f2 . x by A10, A14, A15, A11, A12, FUNCT_1:2; :: thesis: verum

end;

hence f1 = f2 by A5, A7; :: thesis: verum