A1:
dom F = [:J,K:]
by FUNCT_2:def 1;
reconsider F' = F as ManySortedSet of ;
for j being set st j in J holds
(curry F') . j is Function of ((J --> K) . j),((J --> D) . j)
proof
let j be
set ;
:: thesis: ( j in J implies (curry F') . j is Function of ((J --> K) . j),((J --> D) . j) )
assume A2:
j in J
;
:: thesis: (curry F') . j is Function of ((J --> K) . j),((J --> D) . j)
then A3:
(
(J --> K) . j = K &
(J --> D) . j = D )
by FUNCOP_1:13;
J = dom (curry F)
by A1, FUNCT_5:31;
then reconsider G =
(curry F') . j as
Function by A2, FUNCT_5:37;
consider g being
Function such that A4:
(curry F') . j = g
and A5:
dom g = K
and A6:
rng g c= rng F'
and
for
k being
set st
k in K holds
g . k = F' . j,
k
by A1, A2, FUNCT_5:36;
rng F c= D
;
then
rng g c= D
by A6, XBOOLE_1:1;
then reconsider g =
g as
Function of
K,
D by A5, FUNCT_2:def 1, RELSET_1:11;
G = g
by A4;
hence
(curry F') . j is
Function of
((J --> K) . j),
((J --> D) . j)
by A3;
:: thesis: verum
end;
hence
curry F is DoubleIndexedSet of J --> K,D
by PBOOLE:def 18; :: thesis: verum