:: deftheorem defines curry ISOCAT_2:def 2 :
for A, B, C being Category
for F being Functor of [:A,B:],C
for f being Morphism of A holds curry (F,f) = (curry F) . f;