dom (Euler_factorization_2 n) = support (ppf n) by Def3;
hence dom (Euler_factorization_2 n) is finite ; :: thesis: verum