let L be non trivial comRing; :: thesis: for x being Element of L
for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds
x is_a_root_of p
let x be Element of L; :: thesis: for p, q being Polynomial of L st p = <%(- x),(1. L)%> *' q holds
x is_a_root_of p
let p, q be Polynomial of L; :: thesis: ( p = <%(- x),(1. L)%> *' q implies x is_a_root_of p )
assume A1: p = <%(- x),(1. L)%> *' q ; :: thesis: x is_a_root_of p
A2: eval (<%(- x),(1. L)%>,x) = (- x) + x by POLYNOM5:47
.= 0. L by RLVECT_1:5 ;
thus eval (p,x) = (eval (<%(- x),(1. L)%>,x)) * (eval (q,x)) by A1, POLYNOM4:24
.= 0. L by A2 ; :: according to POLYNOM5:def 7 :: thesis: verum