let F be DoubleIndexedSet of K,D; :: thesis: F is V9()

for j being object st j in dom F holds

not F . j is empty

for j being object st j in dom F holds

not F . j is empty

proof

hence
F is V9()
by FUNCT_1:def 9; :: thesis: verum
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;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