let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 A1: ( p1 divides p2 & p1 is with_roots ) ; :: thesis: p1,p2 have_common_roots

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

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

p2 mod p1 = 0_. L by A1;
then 0_. L = p2 - (0_. L) by A2, POLYNOM3:34
.= p2 + (0_. L) by HURWITZ:9 ;
then A3: 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 7;
then 0. L is_a_common_root_of p1,p2 by A2, A3;
hence p1,p2 have_common_roots ; :: thesis: verum

end;

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

then consider s being Polynomial of L such that
A4: s *' p1 = p2 by A1, HURWITZ:34;
consider x being Element of L such that
A5: x is_a_root_of p1 by A1, POLYNOM5:def 8;
A6: eval (p1,x) = 0. L by A5, POLYNOM5:def 7;
eval (p2,x) = (eval (s,x)) * (eval (p1,x)) by A4, POLYNOM4:24
.= 0. L by A6 ;
then x is_a_root_of p2 by POLYNOM5:def 7;
then x is_a_common_root_of p1,p2 by A5;
hence p1,p2 have_common_roots ; :: thesis: verum

end;

end;