let n be non zero Nat; :: thesis: support (Euler_factorization_1 n) = dom (Euler_factorization_1 n)
set f = Euler_factorization_1 n;
thus support (Euler_factorization_1 n) c= dom (Euler_factorization_1 n) by PRE_POLY:37; :: according to XBOOLE_0:def 10 :: thesis: dom (Euler_factorization_1 n) c= support (Euler_factorization_1 n)
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in dom (Euler_factorization_1 n) or p in support (Euler_factorization_1 n) )
assume A1: p in dom (Euler_factorization_1 n) ; :: thesis: p in support (Euler_factorization_1 n)
then reconsider p = p as Prime by Th27;
ex c being non zero Nat st
( c = p |-count n & (Euler_factorization_1 n) . p = p |^ (c - 1) ) by A1, Def2;
hence p in support (Euler_factorization_1 n) by PRE_POLY:def 7; :: thesis: verum