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