:: deftheorem Def1 defines uncurrying WAYBEL27:def 1 :
for F being Function holds
( F is uncurrying iff ( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = uncurry f ) ) );