for X being set
for S being finite Subset of X
for n being Element of NAT st ( S is empty or n = 0 ) holds
(S,n) -bag = EmptyBag X