theorem Th22: :: POLYNOM9:22

for i, k being Nat
for X being set
for x being object
for b being bag of X holds b +* (x,(i + k)) = (b +* (x,i)) + ((EmptyBag X) +* (x,k))