for J, K, D being non empty set
for j being Element of J
for k being Element of K
for F being Function of [:J,K:],D holds
( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k )