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