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