let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 )
assume z is_a_root_of p ; :: thesis: rpoly 1,z divides p
then consider s being Polynomial of L such that
A1: p = (rpoly 1,z) *' s by Th33;
(rpoly 1,z) . 1 = 1_ L by Lm11;
then rpoly 1,z <> 0_. L by FUNCOP_1:13;
hence rpoly 1,z divides p by A1, Th34; :: thesis: verum