for n being Nat holds support (pfexp n) c= SetPrimes