set f = pfexp 1;
assume not support (pfexp 1) is empty ; :: thesis: contradiction
then consider x being set such that
A1: x in support (pfexp 1) by XBOOLE_0:def 1;
(pfexp 1) . x <> 0 by A1, POLYNOM1:def 7;
hence contradiction by Th39, POLYNOM1:56; :: thesis: verum