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 = f " (SubFuncs (rng f)) & ( for x being set 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 = f " (SubFuncs (rng f)) & ( for x being set 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 = 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: f1 = f2

now

let x be set ; :: 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 & dom g = dom (doms f) & ( for x being set st x in dom (doms f) holds
g . x in (doms f) . x ) ) by CARD_3:def 5;
consider h1 being Function such that
A11: ( f1 . g = h1 & dom h1 = f " (SubFuncs (rng f)) & ( for y being set st y in dom h1 holds
h1 . y = (uncurry f) . y,(g . y) ) ) by A6, A9, A10;
consider h2 being Function such that
A12: ( f2 . g = h2 & dom h2 = f " (SubFuncs (rng f)) & ( for y being set st y in dom h2 holds
h2 . y = (uncurry f) . y,(g . y) ) ) by A8, A9, A10;

now

let z be set ; :: thesis: ( z in f " (SubFuncs (rng f)) implies h1 . z = h2 . z )
assume z in f " (SubFuncs (rng f)) ; :: thesis: h1 . z = h2 . z
then ( h1 . z = (uncurry f) . z,(g . z) & h2 . z = (uncurry f) . z,(g . z) ) by A11, A12;
hence h1 . z = h2 . z ; :: thesis: verum

end;

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

end;

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