let L be non empty right_complementable left-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
let p1, p2 be 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
let x be Element of L; ( x is_a_common_root_of p1,p2 implies x is_a_root_of p1 + p2 )
assume
x is_a_common_root_of p1,p2
; x is_a_root_of p1 + p2
then
( x is_a_root_of p1 & x is_a_root_of p2 )
;
then A1:
( eval (p1,x) = 0. L & eval (p2,x) = 0. L )
by POLYNOM5:def 7;
eval ((p1 + p2),x) =
(0. L) + (0. L)
by A1, POLYNOM4:19
.=
0. L
by RLVECT_1:def 4
;
hence
x is_a_root_of p1 + p2
by POLYNOM5:def 7; verum