support (Euler_factorization_1 n) c= dom (Euler_factorization_1 n) by PRE_POLY:37;
hence support (Euler_factorization_1 n) is finite ; :: according to PRE_POLY:def 8 :: thesis: verum