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