A1: dom (Euler_factorization 1) = support (ppf 1) by Def1;
support (ppf 1) = support (pfexp 1) by NAT_3:def 9;
hence Euler_factorization 1 is empty by A1; :: thesis: verum