let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; for p being even Polynomial of L
for q being odd 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 be even Polynomial of L; for q being odd 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 q be odd 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 x be Element of L; ( x is_a_common_root_of p,q implies - x is_a_root_of p + q )
assume A1:
x is_a_common_root_of p,q
; - x is_a_root_of p + q
then A2:
eval (p,x) = 0. L
by POLYNOM5:def 7;
eval ((p + q),(- x)) =
(eval (p,(- x))) + (eval (q,(- x)))
by POLYNOM4:19
.=
(eval (p,x)) + (eval (q,(- x)))
by Th24
.=
(eval (p,x)) + (- (eval (q,x)))
by Th25
.=
(0. L) + (- (0. L))
by A2, A1, POLYNOM5:def 7
.=
0. L
by RLVECT_1:5
;
hence
- x is_a_root_of p + q
by POLYNOM5:def 7; verum