let J, K, D be non empty set ; :: thesis: 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 )
let j be Element of J; :: thesis: 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 )
let k be Element of K; :: thesis: 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 )
let F be Function of [:J,K:],D; :: thesis: ( dom (curry F) = J & dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k )
thus dom (curry F) = proj1 (dom F) by FUNCT_5:def 1
.= proj1 [:J,K:] by FUNCT_2:def 1
.= J by FUNCT_5:9 ; :: thesis: ( dom ((curry F) . j) = K & F . (j,k) = ((curry F) . j) . k )
dom F = [:J,K:] by FUNCT_2:def 1;
then ex g being Function st
( (curry F) . j = g & dom g = K & rng g c= rng F & ( for i being object st i in K holds
g . i = F . (j,i) ) ) by FUNCT_5:29;
hence dom ((curry F) . j) = K ; :: thesis: F . (j,k) = ((curry F) . j) . k
[j,k] in [:J,K:] ;
then [j,k] in dom F by FUNCT_2:def 1;
hence F . (j,k) = ((curry F) . j) . k by FUNCT_5:20; :: thesis: verum