let F be DoubleIndexedSet of K,D; :: thesis: F is non-empty
for j being object st j in dom F holds
not F . j is empty

proof

let j be object ; :: thesis: ( j in dom F implies not F . j is empty )
set k = the Element of K . j;
assume j in dom F ; :: thesis: not F . j is empty
then A1: j in J ;
then F . j is Function of (K . j),D by Th6;
then dom (F . j) = K . j by FUNCT_2:def 1;
then [ the Element of K . j,((F . j) . the Element of K . j)] in F . j by A1, FUNCT_1:def 2;
hence not F . j is empty ; :: thesis: verum

end;

hence F is non-empty by FUNCT_1:def 9; :: thesis: verum