theorem Th7: :: POLYRED:7

for n being Ordinal
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for m being Monomial of n,L
for b being bag of n holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)