let R be Field; :: thesis: for p being Polynomial of R
for a being Element of R st a is_a_root_of p holds
p = (p div (rpoly (1,a))) *' (rpoly (1,a))
let p be Polynomial of R; :: thesis: for a being Element of R st a is_a_root_of p holds
p = (p div (rpoly (1,a))) *' (rpoly (1,a))
let a be Element of R; :: thesis: ( a is_a_root_of p implies p = (p div (rpoly (1,a))) *' (rpoly (1,a)) )
assume A1: a is_a_root_of p ; :: thesis: p = (p div (rpoly (1,a))) *' (rpoly (1,a))
set D = p div (rpoly (1,a));
set RP = rpoly (1,a);
A2: (- ((p div (rpoly (1,a))) *' (rpoly (1,a)))) + ((p div (rpoly (1,a))) *' (rpoly (1,a))) = ((p div (rpoly (1,a))) *' (rpoly (1,a))) - ((p div (rpoly (1,a))) *' (rpoly (1,a)))
.= 0_. R by POLYNOM3:29 ;
p mod (rpoly (1,a)) = 0_. R by A1, HURWITZ:35, HURWITZ:def 7;
then (p - ((p div (rpoly (1,a))) *' (rpoly (1,a)))) + ((p div (rpoly (1,a))) *' (rpoly (1,a))) = (0_. R) + ((p div (rpoly (1,a))) *' (rpoly (1,a))) by HURWITZ:def 6;
then p + (0_. R) = (p div (rpoly (1,a))) *' (rpoly (1,a)) by A2, POLYNOM3:26;
hence p = (p div (rpoly (1,a))) *' (rpoly (1,a)) ; :: thesis: verum