for L being non empty right_complementable distributive add-associative right_zeroed associative commutative doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)