:: deftheorem Def1 defines Euler_factorization NUMBER08:def 1 :
for n being non zero Nat
for b₂ being Function holds
( b₂ = Euler_factorization 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) - (p |^ (c - 1)) ) ) ) );