let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L st p1 divides p2 & p1 is with_roots holds
p1,p2 have_common_roots
let p1, p2 be Polynomial of L; :: thesis: ( p1 divides p2 & p1 is with_roots implies p1,p2 have_common_roots )
assume AS: ( p1 divides p2 & p1 is with_roots ) ; :: thesis: p1,p2 have_common_roots

per cases ( p1 = 0_. L or p1 <> 0_. L ) ;

suppose A: p1 = 0_. L ; :: thesis: p1,p2 have_common_roots

p2 mod p1 = 0_. L by AS, HURWITZ:def 7;
then 0_. L = p2 - (0_. L) by A, POLYNOM3:34
.= p2 + (0_. L) by HURWITZ:9 ;
then B: p2 = 0_. L by POLYNOM3:28;
eval ((0_. L),(0. L)) = 0. L by POLYNOM4:17;
then 0. L is_a_root_of 0_. L by POLYNOM5:def 6;
then 0. L is_a_common_root_of p1,p2 by A, B, root1;
hence p1,p2 have_common_roots by root2; :: thesis: verum

end;

suppose p1 <> 0_. L ; :: thesis: p1,p2 have_common_roots

then consider s being Polynomial of L such that
A: s *' p1 = p2 by AS, HURWITZ:34;
consider x being Element of L such that
B: x is_a_root_of p1 by AS, POLYNOM5:def 7;
C: eval (p1,x) = 0. L by B, POLYNOM5:def 6;
eval (p2,x) = (eval (s,x)) * (eval (p1,x)) by A, POLYNOM4:24
.= 0. L by C, VECTSP_1:6 ;
then x is_a_root_of p2 by POLYNOM5:def 6;
then x is_a_common_root_of p1,p2 by B, root1;
hence p1,p2 have_common_roots by root2; :: thesis: verum

end;

end;