reconsider F9 = F as ManySortedSet of [:J,K:] ;
A1: dom F = [:J,K:] by FUNCT_2:def 1;
for j being object st j in J holds
(curry F9) . j is Function of ((J --> K) . j),((J --> D) . j)

proof

let j be object ; :: thesis: ( j in J implies (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) )
assume A2: j in J ; :: thesis: (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j)
then consider g being Function such that
A3: (curry F9) . j = g and
A4: dom g = K and
A5: rng g c= rng F9 and
for k being object st k in K holds
g . k = F9 . (j,k) by A1, FUNCT_5:29;
J = dom (curry F) by A1, FUNCT_5:24;
then reconsider G = (curry F9) . j as Function ;
rng F c= D ;
then rng g c= D by A5;
then reconsider g = g as Function of K,D by A4, FUNCT_2:def 1, RELSET_1:4;
A6: G = g by A3;
(J --> K) . j = K by A2, FUNCOP_1:7;
hence (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) by A2, A6, FUNCOP_1:7; :: thesis: verum

end;

hence curry F is DoubleIndexedSet of J --> K,D by PBOOLE:def 15; :: thesis: verum