theorem Th4: :: UPROOTS:7

for X being set
for S being finite Subset of X
for n being Element of NAT
for i being set st i in S holds
((S,n) -bag) . i = n