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 )
for x being set holds
( x in rng f iff ( x in rng f & x is Function ) )

proof

let y be set ; :: thesis: ( y in rng f iff ( y in rng f & y is Function ) )
( y in rng f implies y is Function )

proof

assume y in rng f ; :: thesis: y is Function
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def 5;
hence y is Function ; :: thesis: verum

end;

hence ( y in rng f iff ( y in rng f & y is Function ) ) ; :: thesis: verum

end;

then A3: SubFuncs (rng f) = rng f by FUNCT_6:def 1;
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 A4: 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 A5: g in product (doms f) ; :: thesis: F . g = f .. g
then consider h being Function such that
A6: F . g = h and
A7: dom h = f " (SubFuncs (rng f)) and
A8: for x being set st x in dom h holds
h . x = (uncurry f) . x,(g . x) by A4, FUNCT_6:def 7;
A9: dom h = dom f by A3, A7, RELAT_1:169;
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 A10: x in dom f ; :: thesis: h . x = (f . x) . (g . x)
then x in dom (doms f) by A7, A9, FUNCT_6:def 2;
then g . x in (doms f) . x by A5, CARD_3:18;
then A11: g . x in dom (f . x) by A10, FUNCT_6:31;
thus h . x = f .. x,(g . x) by A8, A9, A10
.= (f . x) . (g . x) by A10, A11, FUNCT_5:45 ; :: thesis: verum

end;

hence F . g = f .. g by A6, A9, PRALG_1:def 17; :: thesis: verum

end;

assume A12: for g being Function st g in product (doms f) holds
F . g = f .. g ; :: thesis: F = Frege f
A13: for g being Function st g in product (doms f) holds
ex h being Function st
( F . 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) ) )

proof

let g be Function; :: thesis: ( g in product (doms f) implies ex h being Function st
( F . 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) ) ) )
assume A14: g in product (doms f) ; :: thesis: ex h being Function st
( F . 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) ) )
F . g = f .. g by A12, A14;
then A15: dom (F . g) = dom f by PRALG_1:def 17;
take F . g ; :: thesis: ( F . g = F . g & dom (F . g) = f " (SubFuncs (rng f)) & ( for x being set st x in dom (F . g) holds
(F . g) . x = (uncurry f) . x,(g . x) ) )
thus F . g = F . g ; :: thesis: ( dom (F . g) = f " (SubFuncs (rng f)) & ( for x being set st x in dom (F . g) holds
(F . g) . x = (uncurry f) . x,(g . x) ) )
thus A16: dom (F . g) = f " (SubFuncs (rng f)) by A3, A15, RELAT_1:169; :: thesis: for x being set st x in dom (F . g) holds
(F . g) . x = (uncurry f) . x,(g . x)
let x be set ; :: thesis: ( x in dom (F . g) implies (F . g) . x = (uncurry f) . x,(g . x) )
assume A17: x in dom (F . g) ; :: thesis: (F . g) . x = (uncurry f) . x,(g . x)
then x in dom (doms f) by A16, FUNCT_6:def 2;
then g . x in (doms f) . x by A14, CARD_3:18;
then A18: g . x in dom (f . x) by A15, A17, FUNCT_6:31;
thus (F . g) . x = (f .. g) . x by A12, A14
.= (f . x) . (g . x) by A15, A17, PRALG_1:def 17
.= (uncurry f) . x,(g . x) by A15, A17, A18, FUNCT_5:45 ; :: thesis: verum

end;

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