( dom (F . j) = K . j & dom F = J ) by FUNCT_2:def 1, PARTFUN1:def 2;
then F .. (j,k) = (F . j) . k by FUNCT_5:38;
hence F .. (j,k) is Element of D ; :: thesis: verum