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

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