for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of L
for z being Element of L st z is_a_root_of p holds
rpoly (1,z) divides p