let n be non zero Nat; :: thesis: support (Euler_factorization n) = dom (Euler_factorization n)
set f = Euler_factorization n;
thus support (Euler_factorization n) c= dom (Euler_factorization n) by PRE_POLY:37; :: according to XBOOLE_0:def 10 :: thesis: dom (Euler_factorization n) c= support (Euler_factorization n)
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in dom (Euler_factorization n) or p in support (Euler_factorization n) )
assume A1: p in dom (Euler_factorization n) ; :: thesis: p in support (Euler_factorization n)
then reconsider p = p as Prime by Th17;
consider c being non zero Nat such that
A2: ( c = p |-count n & (Euler_factorization n) . p = (p |^ c) - (p |^ (c - 1)) ) by A1, Def1;
c - 1 < c - 0 by XREAL_1:15;
then (Euler_factorization n) . p <> 0 by A2, NAT_6:2;
hence p in support (Euler_factorization n) by PRE_POLY:def 7; :: thesis: verum