theorem :: MOEBIUS2:33

for p being Prime
for f being positive-yielding bag of Seg p st f = p |-> p holds
Product f = p |^ p