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 ;
( j in J implies (curry F9) . j is Function of ((J --> K) . j),((J --> D) . j) )
assume A2:
j in J
;
(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;
verum
end;
hence
curry F is DoubleIndexedSet of J --> K,D
by PBOOLE:def 15; verum