theorem :: NUMBER08:46

for n being non zero Nat holds Product ((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) divides (n - 1) ! by Th45, Th44;