for X being non empty set
for a being Element of X
for n being Element of NAT holds card (({a},n) -bag) = n