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