theorem Th33: :: NUMBER08:33

for n being non zero Nat holds Product ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) divides n