theorem :: RATFUNC1:15

for L being non empty right_complementable distributive Abelian add-associative right_zeroed unital doubleLoopStr
for p1, p2 being Polynomial of L
for x being Element of L st x is_a_common_root_of p1,p2 holds
x is_a_root_of - (p1 + p2) by Th13, Th14;