let F be Field; :: thesis: for p being Ppoly of F
for q being monic Polynomial of F
for a being Element of F holds
( q divides (rpoly (1,a)) *' p iff ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) )
let p be Ppoly of F; :: thesis: for q being monic Polynomial of F
for a being Element of F holds
( q divides (rpoly (1,a)) *' p iff ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) )
let q be monic Polynomial of F; :: thesis: for a being Element of F holds
( q divides (rpoly (1,a)) *' p iff ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) )
let a be Element of F; :: thesis: ( q divides (rpoly (1,a)) *' p iff ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) )

A: now :: thesis: ( ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) implies q divides (rpoly (1,a)) *' p )

assume ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) ; :: thesis: q divides (rpoly (1,a)) *' p

per cases then ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) ;

suppose q divides p ; :: thesis: q divides (rpoly (1,a)) *' p

then consider u being Polynomial of F such that
B: p = q *' u by RING_4:1;
q *' (u *' (rpoly (1,a))) = (rpoly (1,a)) *' p by B, POLYNOM3:33;
hence q divides (rpoly (1,a)) *' p by RING_4:1; :: thesis: verum

end;

suppose ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ; :: thesis: q divides (rpoly (1,a)) *' p

then consider r being Polynomial of F such that
B: ( r divides p & q = (rpoly (1,a)) *' r ) ;
consider u being Polynomial of F such that
C: p = r *' u by B, RING_4:1;
q *' u = (rpoly (1,a)) *' p by C, B, POLYNOM3:33;
hence q divides (rpoly (1,a)) *' p by RING_4:1; :: thesis: verum

end;

end;

end;

now :: thesis: ( q divides (rpoly (1,a)) *' p & not q divides p implies ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) )

assume B1: q divides (rpoly (1,a)) *' p ; :: thesis: ( not q divides p implies ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) )
rpoly (1,a) is Ppoly of F by RING_5:51;
then (rpoly (1,a)) *' p is Ppoly of F by RING_5:52;
then reconsider rp = (rpoly (1,a)) *' p as Ppoly of F, BRoots ((rpoly (1,a)) *' p) by RING_5:59;
B3: q divides rp by B1;
assume B4: not q divides p ; :: thesis: ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r )

now :: thesis: not q is constant

assume q is constant ; :: thesis: contradiction
then q = 1_. F by lemconst;
then q *' p = p ;
hence contradiction by B4, RING_4:1; :: thesis: verum

end;

then consider B2 being non zero bag of the carrier of F such that
B6: ( q is Ppoly of F,B2 & B2 divides BRoots ((rpoly (1,a)) *' p) ) by B3, ppolydiv;
p is Ppoly of F, BRoots p by RING_5:59;
then B7: ( not B2 divides BRoots p & BRoots q = B2 ) by B6, B4, ppolydiv, RING_5:55;
then consider o being object such that
B8: (BRoots q) . o > (BRoots p) . o by PRE_POLY:def 11;
rpoly (1,a) is Ppoly of F, Bag {a} by RING_5:57;
then BRoots (rpoly (1,a)) = Bag {a} by RING_5:55;
then B9: BRoots ((rpoly (1,a)) *' p) = (Bag {a}) + (BRoots p) by UPROOTS:56;

now :: thesis: not o <> a

assume o <> a ; :: thesis: contradiction
then not o in {a} by TARSKI:def 1;
then 0 = (({a},1) -bag) . o by UPROOTS:6
.= (Bag {a}) . o by RING_5:def 1 ;
then (BRoots ((rpoly (1,a)) *' p)) . o = 0 + ((BRoots p) . o) by B9, PRE_POLY:def 5;
hence contradiction by B6, B8, B7, PRE_POLY:def 11; :: thesis: verum

end;

then (BRoots q) . a >= 1 by B8, NAT_1:14;
then multiplicity (q,a) >= 1 by UPROOTS:def 9;
then eval (q,a) = 0. F by UPROOTS:52, POLYNOM5:def 7;
then consider r being Polynomial of F such that
B8: q = (rpoly (1,a)) *' r by RING_4:1, RING_5:11;
thus ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) by B1, B8, ZZ3z; :: thesis: verum

end;

hence ( q divides (rpoly (1,a)) *' p iff ( q divides p or ex r being Polynomial of F st
( r divides p & q = (rpoly (1,a)) *' r ) ) ) by A; :: thesis: verum