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