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;

hence doms F = K by A2, A1, A3, FUNCT_1:2; :: thesis: verum

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

( dom K = J & F " (rng F) = dom F )
by PARTFUN1:def 2, RELAT_1:134;(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;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

hence doms F = K by A2, A1, A3, FUNCT_1:2; :: thesis: verum