theorem :: RATFUNC1:16

for L being non empty right_complementable distributive Abelian add-associative right_zeroed unital doubleLoopStr
for p, q being 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