let J be set ; :: thesis: for D being non empty set
for K being ManySortedSet of
for F being DoubleIndexedSet of K,D holds doms F = K
let D be non empty set ; :: thesis: for K being ManySortedSet of
for F being DoubleIndexedSet of K,D holds doms F = K
let K be ManySortedSet of ; :: 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 F = J & dom K = J & F " (rng F) = dom F & dom (doms F) = F " (SubFuncs (rng F)) ) by FUNCT_6:def 2, PARTFUN1:def 4, RELAT_1:169;
A2: SubFuncs (rng F) = rng F

proof

thus SubFuncs (rng F) c= rng F by FUNCT_6:27; :: according to XBOOLE_0:def 10 :: thesis: rng F c= SubFuncs (rng F)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in SubFuncs (rng F) )
assume A3: x in rng F ; :: thesis: x in SubFuncs (rng F)
then ex y being set st
( y in dom F & x = F . y ) by FUNCT_1:def 5;
hence x in SubFuncs (rng F) by A3, FUNCT_6:def 1; :: thesis: verum

end;

now

let j be set ; :: thesis: ( j in J implies (doms F) . j = K . j )
assume A4: j in J ; :: thesis: (doms F) . j = K . j
set f = F . j;
(J --> D) . j = D by A4, FUNCOP_1:13;
then ( (doms F) . j = dom (F . j) & F . j is Function of (K . j),D ) by A1, A4, FUNCT_6:31, PBOOLE:def 18;
hence (doms F) . j = K . j by FUNCT_2:def 1; :: thesis: verum

end;

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