let n be natural number ; :: thesis: for x being set st x in support (pfexp n) holds
x is Prime
let x be set ; :: thesis: ( x in support (pfexp n) implies x is Prime )
set f = pfexp n;
assume A1: x in support (pfexp n) ; :: thesis: x is Prime
support (pfexp n) c= dom (pfexp n) by POLYNOM1:41;
hence x is Prime by A1, Th33; :: thesis: verum