dom (Euler_factorization_1 n) = support (ppf n) by Def2;
hence dom (Euler_factorization_1 n) is finite ; :: thesis: verum