theorem KeyValue: :: MOEBIUS3:45

for m being natural-valued finite-support ManySortedSet of SetPrimes
for p being Prime st support m = {p} holds
Product m = m . p