:: deftheorem Def6 defines Frege FUNCT_6:def 7 :
for f being Function-yielding Function
for b₂ being Function holds
( b₂ = Frege f iff ( dom b₂ = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( b₂ . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) ) ) );