:: deftheorem Def2 defines Euler_factorization_1 NUMBER08:def 2 :
for n being non zero Nat
for b₂ being Function holds
( b₂ = Euler_factorization_1 n iff ( dom b₂ = support (ppf n) & ( for p being Nat st p in dom b₂ holds
ex c being non zero Nat st
( c = p |-count n & b₂ . p = p |^ (c - 1) ) ) ) );