let J be set ; :: thesis: for D being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D holds doms F = K
let D be non empty set ; :: thesis: for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D holds doms F = K
let K be ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,D holds doms F = K
let F be DoubleIndexedSet of K,D; :: thesis: doms F = K
A1: dom (doms F) = dom F by FUNCT_6:def 2;
A2: dom F = J by PARTFUN1:def 2;

A3: now :: thesis: for j being object st j in J holds
(doms F) . j = K . j

let j be object ; :: thesis: ( j in J implies (doms F) . j = K . j )
set f = F . j;
assume A4: j in J ; :: thesis: (doms F) . j = K . j
then (J --> D) . j = D by FUNCOP_1:7;
then A5: F . j is Function of (K . j),D by A4, PBOOLE:def 15;
(doms F) . j = dom (F . j) by A2, A4, FUNCT_6:22;
hence (doms F) . j = K . j by A5, FUNCT_2:def 1; :: thesis: verum

end;

( dom K = J & F " (rng F) = dom F ) by PARTFUN1:def 2, RELAT_1:134;
hence doms F = K by A2, A1, A3, FUNCT_1:2; :: thesis: verum