dom (F . j) = K . j by FUNCT_2:def 1;
hence not rng (F . j) is empty by RELAT_1:65; :: thesis: verum