dom (Euler_factorization_1 n) = support (ppf n) by Def2;
hence dom (Euler_factorization_1 n) c= SetPrimes ; :: according to RELAT_1:def 18 :: thesis: verum