dom (p ^ q) = (dom p) +^ (dom q) by ORDINAL4:def 1;
hence p ^ q is finite by FINSET_1:10; :: thesis: verum