theorem Th12: :: MOEBIUS1:12

for n being Nat
for N being Rbag of NAT st support N = {n} holds
Sum N = N . n