theorem Th7: :: UPROOTS:10

for X being set
for S, T being finite Subset of X
for n being Element of NAT st S misses T holds
((S \/ T),n) -bag = ((S,n) -bag) + ((T,n) -bag)