:: deftheorem defines <: FUNCT_6:def 6 :
for f being Function-yielding Function holds <:f:> = curry ((uncurry' f) | [:(meet (doms f)),(dom f):]);