theorem BZE: :: MOEBIUS2:48

for n being Nat
for p being Prime
for f being bag of SetPrimes st f . p = p |^ n holds
p |-count (Product f) >= n