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