dom (p (#) q) = (dom p) /\ (dom q) by VALUED_1:def 4;
hence p (#) q is finite by FINSET_1:10; :: thesis: verum