let L be non trivial comRing; 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; 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; ( p = <%(- x),(1. L)%> *' q implies x is_a_root_of p )
assume A1:
p = <%(- x),(1. L)%> *' q
; 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
; POLYNOM5:def 7 verum