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