let L be non empty right_complementable unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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
let p, q be Polynomial of L; :: thesis: for x being Element of L st x is_a_common_root_of p,q holds
x is_a_root_of p + q
let x be Element of L; :: thesis: ( x is_a_common_root_of p,q implies x is_a_root_of p + q )
assume x is_a_common_root_of p,q ; :: thesis: x is_a_root_of p + q
then H: ( x is_a_root_of p & x is_a_root_of q ) by root1;
then H1: eval (p,x) = 0. L by POLYNOM5:def 6;
H2: eval (q,x) = 0. L by H, POLYNOM5:def 6;
eval ((p + q),x) = (0. L) + (0. L) by H1, H2, POLYNOM4:19
.= 0. L by RLVECT_1:def 4 ;
hence x is_a_root_of p + q by POLYNOM5:def 6; :: thesis: verum