:: deftheorem Def2 defines Frege PRALG_2:def 2 :
for f being Function-yielding Function
for b₂ being ManySortedFunction of product (doms f) holds
( b₂ = Frege f iff for g being Function st g in product (doms f) holds
b₂ . g = f .. g );