let n be Nat; :: 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;
A1: support (pfexp n) c= dom (pfexp n) by PRE_POLY:37;
assume x in support (pfexp n) ; :: thesis: x is Prime
hence x is Prime by A1, Th33; :: thesis: verum