theorem Th28: :: NUMBER08:28

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