let n be non zero Nat; :: thesis: for p being object st p in dom (Euler_factorization_1 n) holds
p is Prime
let p be object ; :: thesis: ( p in dom (Euler_factorization_1 n) implies p is Prime )
dom (Euler_factorization_1 n) c= SetPrimes by RELAT_1:def 18;
hence ( p in dom (Euler_factorization_1 n) implies p is Prime ) by NEWTON:def 6; :: thesis: verum