:: deftheorem defines -bag UPROOTS:def 2 :
for X being set
for S being finite Subset of X
for n being Element of NAT holds (S,n) -bag = (EmptyBag X) +* (S --> n);