let n be Nat; :: thesis: for x being set st x in dom (pfexp n) holds
x is Prime
let x be set ; :: thesis: ( x in dom (pfexp n) implies x is Prime )
assume x in dom (pfexp n) ; :: thesis: x is Prime
then x in SetPrimes by PARTFUN1:def 2;
hence x is Prime by NEWTON:def 6; :: thesis: verum