theorem Th31: :: NUMBER08:31

for n being non zero Nat holds (EmptyBag SetPrimes) +* (Euler_factorization n) = ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) (#) ((EmptyBag SetPrimes) +* (Euler_factorization_2 n))