let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p being Polynomial of L
for z being Element of L st z is_a_root_of p holds
rpoly (1,z) divides p
let p be Polynomial of L; :: thesis: for z being Element of L st z is_a_root_of p holds
rpoly (1,z) divides p
let z be Element of L; :: thesis: ( z is_a_root_of p implies rpoly (1,z) divides p )
(rpoly (1,z)) . 1 = 1_ L by Lm10;
then A1: rpoly (1,z) <> 0_. L ;
assume z is_a_root_of p ; :: thesis: rpoly (1,z) divides p
then ex s being Polynomial of L st p = (rpoly (1,z)) *' s by Th33;
hence rpoly (1,z) divides p by A1, Th34; :: thesis: verum