theorem Matsu1: :: MOEBIUS2:47

for n being Nat
for p being Prime
for f being bag of SetPrimes st f . p = p |^ n holds
p |^ n divides Product f