theorem :: POLYNOM5:51

for L being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for p being Polynomial of L
for x being Element of L holds len (Subst (p,<%x%>)) <= 1