theorem :: POLYNOM9:23

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