theorem BagValue: :: MOEBIUS3:55

for A being finite Subset of SetPrimes
for i being object st i in support (A -bag) holds
(A -bag) . i = i