let F be Field; :: thesis: for B1 being non zero bag of the carrier of F
for p being Ppoly of F,B1
for q being non constant monic Polynomial of F holds
( q divides p iff ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) )
let B1 be non zero bag of the carrier of F; :: thesis: for p being Ppoly of F,B1
for q being non constant monic Polynomial of F holds
( q divides p iff ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) )
let p be Ppoly of F,B1; :: thesis: for q being non constant monic Polynomial of F holds
( q divides p iff ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) )
let q be non constant monic Polynomial of F; :: thesis: ( q divides p iff ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) )

A: now :: thesis: ( q divides p implies ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) )

assume q divides p ; :: thesis: ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 )
then consider u being Polynomial of F such that
A1: p = q *' u by RING_4:1;
A2: not u is zero by A1;
then reconsider q1 = q as Ppoly of F by A1, FIELD_8:10;
A3: B1 = BRoots p by RING_5:55;
q1 is Ppoly of F, BRoots q1 by RING_5:59;
hence ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) by A3, A1, A2, ZZ1fB; :: thesis: verum

end;

now :: thesis: for B1 being non zero bag of the carrier of F
for p being Ppoly of F,B1
for q being non constant monic Polynomial of F st ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) holds
q divides p

let B1 be non zero bag of the carrier of F; :: thesis: for p being Ppoly of F,B1
for q being non constant monic Polynomial of F st ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) holds
b₅ divides b₄
let p be Ppoly of F,B1; :: thesis: for q being non constant monic Polynomial of F st ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) holds
b₄ divides b₃
let q be non constant monic Polynomial of F; :: thesis: ( ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) implies b₃ divides b₂ )
assume ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) ; :: thesis: b₃ divides b₂
then consider B2 being non zero bag of the carrier of F such that
I3: ( q is Ppoly of F,B2 & B2 divides B1 ) ;
set B3 = B1 -' B2;

per cases ( B1 -' B2 is zero or not B1 -' B2 is zero ) ;

suppose B1 -' B2 is zero ; :: thesis: b₃ divides b₂

then p = q *' (1_. F) by I3, bag6, bag5;
hence q divides p by RING_4:1; :: thesis: verum

end;

suppose not B1 -' B2 is zero ; :: thesis: b₃ divides b₂

then reconsider B3 = B1 -' B2 as non zero bag of the carrier of F ;
set u = the Ppoly of F,B3;
B3 + B2 = B1 by I3, PRE_POLY:47;
then reconsider r = q *' the Ppoly of F,B3 as Ppoly of F,B1 by I3, RING_5:58;
r = p by bag5;
hence q divides p by RING_4:1; :: thesis: verum

end;

end;

end;

hence ( q divides p iff ex B2 being non zero bag of the carrier of F st
( q is Ppoly of F,B2 & B2 divides B1 ) ) by A; :: thesis: verum