let n be non zero Nat; :: thesis: support (Euler_factorization_2 n) = dom (Euler_factorization_2 n)
set f = Euler_factorization_2 n;
thus support (Euler_factorization_2 n) c= dom (Euler_factorization_2 n) by PRE_POLY:37; :: according to XBOOLE_0:def 10 :: thesis: dom (Euler_factorization_2 n) c= support (Euler_factorization_2 n)
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in dom (Euler_factorization_2 n) or p in support (Euler_factorization_2 n) )
assume A1: p in dom (Euler_factorization_2 n) ; :: thesis: p in support (Euler_factorization_2 n)
then reconsider p = p as Prime by Th29;
(Euler_factorization_2 n) . p = p - 1 by A1, Def3;
hence p in support (Euler_factorization_2 n) by PRE_POLY:def 7; :: thesis: verum