theorem Th30: :: NUMBER08:30

for n being non zero Nat holds support (Euler_factorization_2 n) = dom (Euler_factorization_2 n)