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