theorem :: POLYNOM9:24

for X being set
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a1, a2 being Element of L
for b being bag of X holds (Monom (a1,b)) + (Monom (a2,b)) = Monom ((a1 + a2),b)