dom (p ^ q) = (dom p) +^ (dom q) by ORDINAL4:def 1;
then dom (p ^ q) is Element of NAT by ORDINAL1:def 13;
hence p ^ q is finite by Th7; :: thesis: verum