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