theorem bb4: :: RING_5:31

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