:: deftheorem Def3 defines Euler_factorization_2 NUMBER08:def 3 :
for n being non zero Nat
for b₂ being Function holds
( b₂ = Euler_factorization_2 n iff ( dom b₂ = support (ppf n) & ( for p being Nat st p in dom b₂ holds
b₂ . p = p - 1 ) ) );