let L be non empty right_complementable distributive Abelian add-associative right_zeroed unital 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 A1: ( x is_a_root_of p & x is_a_root_of q ) ;
then A2: eval (p,x) = 0. L by POLYNOM5:def 7;
A3: eval (q,x) = 0. L by A1, POLYNOM5:def 7;
eval ((p + q),x) = (0. L) + (0. L) by A2, A3, POLYNOM4:19
.= 0. L by RLVECT_1:def 4 ;
hence x is_a_root_of p + q by POLYNOM5:def 7; :: thesis: verum