dom (p /" q) = (dom p) /\ (dom q) by VALUED_1:16;
hence p /" q is finite by FINSET_1:29; :: thesis: verum