theorem Th33: :: HURWITZ:33

for L being non empty right_complementable 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
ex s being Polynomial of L st p = (rpoly (1,z)) *' s