support f = support (- f) by Th10;
hence - f is finite-support by PRE_POLY:def 8; :: thesis: verum