A1: dom (Frege f) = product (doms f) by FUNCT_6:def 7;
Frege f is Function-yielding

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom (Frege f) or (Frege f) . x is set )
assume A2: x in dom (Frege f) ; :: thesis: (Frege f) . x is set
then reconsider g = x as Function by A1;
ex h being Function st
( (Frege f) . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) by A1, A2, FUNCT_6:def 7;
hence (Frege f) . x is set ; :: thesis: verum

end;

hence Frege f is ManySortedFunction of product (doms f) by A1, PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum