dom p = dom (abs p) by VALUED_1:def 11;
hence abs p is finite by FINSET_1:10; :: thesis: verum