theorem Th18: :: NUMBER08:18

for n being non zero Nat
for p being Nat st p in dom (Euler_factorization n) holds
ex c being non zero Nat st
( c = p |-count n & (Euler_factorization n) . p = (p |^ (c - 1)) * (p - 1) )