p - q = p + (- q) by POLYNOM1:def 6;
hence p - q is finite-Support ; :: thesis: verum