for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds ((monomial (a,n)) *' p) . (x + n) = a * (p . x)