for n being Nat
for x being set st x in dom (pfexp n) holds
x is Prime