dom p = dom (p ") by VALUED_1:def 7;
hence p " is finite by FINSET_1:29; :: thesis: verum