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

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