let n be non zero Nat; :: thesis: ( support (pfexp n) = {} implies n = 1 )
assume that
A1: support (pfexp n) = {} and
A2: n <> 1 ; :: thesis: contradiction
n >= 0 + 1 by NAT_1:13;
then n > 1 by A2, XXREAL_0:1;
then n >= 1 + 1 by NAT_1:13;
then consider p being Element of NAT such that
A3: p is prime and
A4: p divides n by INT_2:31;
p > 1 by A3;
then p |-count n <> 0 by A4, Th27;
then (pfexp n) . p <> 0 by A3, Def8;
hence contradiction by A1, PRE_POLY:def 7; :: thesis: verum