for L being non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being even Polynomial of L
for q being odd Polynomial of L
for x being Element of L st x is_a_common_root_of p,q holds
- x is_a_root_of p + q