let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: 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; :: thesis: 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; :: 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 A1: x is_a_common_root_of p,q ; :: thesis: - 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; :: thesis: verum