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)

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

hence
curry F is DoubleIndexedSet of J --> K,D
by PBOOLE:def 15; :: thesis: verum
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;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