per cases ( not p is constant or p is constant ) ;

suppose not p is constant ; :: thesis: MonicDivisors p is finite

then deg p > 0 by RATFUNC1:def 2;
then reconsider u = p as non constant Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10, RING_4:def 4;
set E = the SplittingField of u;
u splits_in the SplittingField of u by FIELD_8:def 1;
then consider a being non zero Element of the SplittingField of u, q being Ppoly of the SplittingField of u such that
A: u = a * q by FIELD_4:def 5;
q is Element of the carrier of (Polynom-Ring the SplittingField of u) by POLYNOM3:def 10;
then MonicDivisors q = MonicDivisors (a * q) by diveq;
then B: MonicDivisors u c= MonicDivisors q by A, divfin1;
consider n being Nat such that
C: ( card (MonicDivisors q) = n & n <= 2 |^ (deg q) ) by divfin2;
MonicDivisors q is finite by C;
hence MonicDivisors p is finite by B; :: thesis: verum

end;

suppose A: p is constant ; :: thesis: MonicDivisors p is finite

now :: thesis: for o being object st o in { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } holds
o in {(1_. F)}

let o be object ; :: thesis: ( o in { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } implies o in {(1_. F)} )
assume o in { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } ; :: thesis: o in {(1_. F)}
then consider r being monic Element of the carrier of (Polynom-Ring F) such that
B: ( o = r & r divides p ) ;
reconsider r = r as monic Polynomial of F ;
D: deg r <= deg p by B, RING_5:13;
deg p <= 0 by A, RATFUNC1:def 2;
then r = 1_. F by D, RATFUNC1:def 2, lemconst;
hence o in {(1_. F)} by B, TARSKI:def 1; :: thesis: verum

end;

then MonicDivisors p c= {(1_. F)} ;
hence MonicDivisors p is finite ; :: thesis: verum

end;

end;