dom p = dom (c (#) p) by VALUED_1:def 5;
hence c (#) p is finite by FINSET_1:10; :: thesis: verum