theorem Th13: :: INT_7:13

for p being bag of SetPrimes st p is prime-factorization-like holds
Product p <> 0