let L be non empty right_complementable distributive Abelian add-associative right_zeroed unital doubleLoopStr ; :: thesis: for p being Polynomial of L
for x being Element of L st x is_a_root_of p holds
x is_a_root_of - p
let p be Polynomial of L; :: thesis: for x being Element of L st x is_a_root_of p holds
x is_a_root_of - p
let x be Element of L; :: thesis: ( x is_a_root_of p implies x is_a_root_of - p )
assume A1: x is_a_root_of p ; :: thesis: x is_a_root_of - p
eval ((- p),x) = - (eval (p,x)) by POLYNOM4:20
.= - (0. L) by A1, POLYNOM5:def 7
.= 0. L by RLVECT_1:12 ;
hence x is_a_root_of - p by POLYNOM5:def 7; :: thesis: verum