let F be ManySortedFunction of product (doms f); :: thesis: ( F = Frege f iff for g being Function st g in product (doms f) holds
F . g = f .. g )
thus ( F = Frege f implies for g being Function st g in product (doms f) holds
F . g = f .. g ) :: thesis: ( ( for g being Function st g in product (doms f) holds
F . g = f .. g ) implies F = Frege f )

proof

assume A3: F = Frege f ; :: thesis: for g being Function st g in product (doms f) holds
F . g = f .. g
let g be Function; :: thesis: ( g in product (doms f) implies F . g = f .. g )
assume A4: g in product (doms f) ; :: thesis: F . g = f .. g
then consider h being Function such that
A5: F . g = h and
A6: dom h = dom f and
A7: for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) by A3, FUNCT_6:def 7;
A8: dom h = dom f by A6;
for x being set st x in dom f holds
h . x = (f . x) . (g . x)

proof

let x be set ; :: thesis: ( x in dom f implies h . x = (f . x) . (g . x) )
assume A9: x in dom f ; :: thesis: h . x = (f . x) . (g . x)
then x in dom (doms f) by FUNCT_6:def 2;
then g . x in (doms f) . x by A4, CARD_3:9;
then A10: g . x in dom (f . x) by A9, FUNCT_6:22;
thus h . x = f .. (x,(g . x)) by A7, A8, A9
.= (f . x) . (g . x) by A9, A10, FUNCT_5:38 ; :: thesis: verum

end;

hence F . g = f .. g by A5, A8, PRALG_1:def 17; :: thesis: verum

end;

assume A11: for g being Function st g in product (doms f) holds
F . g = f .. g ; :: thesis: F = Frege f
A12: for g being Function st g in product (doms f) holds
ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )

proof

let g be Function; :: thesis: ( g in product (doms f) implies ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) )
assume A13: g in product (doms f) ; :: thesis: ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )
F . g = f .. g by A11, A13;
then A14: dom (F . g) = dom f by PRALG_1:def 17;
take F . g ; :: thesis: ( F . g = F . g & dom (F . g) = dom f & ( for x being object st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x)) ) )
thus F . g = F . g ; :: thesis: ( dom (F . g) = dom f & ( for x being object st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x)) ) )
thus dom (F . g) = dom f by A14; :: thesis: for x being object st x in dom (F . g) holds
(F . g) . x = (uncurry f) . (x,(g . x))
let x be object ; :: thesis: ( x in dom (F . g) implies (F . g) . x = (uncurry f) . (x,(g . x)) )
assume A15: x in dom (F . g) ; :: thesis: (F . g) . x = (uncurry f) . (x,(g . x))
then x in dom (doms f) by A14, FUNCT_6:def 2;
then g . x in (doms f) . x by A13, CARD_3:9;
then A16: g . x in dom (f . x) by A14, A15, FUNCT_6:22;
thus (F . g) . x = (f .. g) . x by A11, A13
.= (f . x) . (g . x) by A14, A15, PRALG_1:def 17
.= (uncurry f) . (x,(g . x)) by A14, A15, A16, FUNCT_5:38 ; :: thesis: verum

end;

dom F = product (doms f) by PARTFUN1:def 2;
hence F = Frege f by A12, FUNCT_6:def 7; :: thesis: verum