:: deftheorem Def2 defines currying WAYBEL27:def 2 :
for F being Function holds
( F is currying iff ( ( for x being set st x in dom F holds
( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds
F . f = curry f ) ) );