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:48
.= 0. L by RLVECT_1:16 ;
thus eval p,x = (eval <%(- x),(1. L)%>,x) * (eval q,x) by A1, POLYNOM4:27
.= 0. L by A2, VECTSP_1:39 ; :: according to POLYNOM5:def 6 :: thesis: verum