let F be Field; :: thesis: for p being non zero Polynomial of F holds card (MonicDivisors p) <= 2 |^ (deg p)
let p be non zero Polynomial of F; :: thesis: card (MonicDivisors p) <= 2 |^ (deg p)

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

suppose not p is constant ; :: thesis: card (MonicDivisors p) <= 2 |^ (deg p)

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 C: card (MonicDivisors u) <= card (MonicDivisors q) by NAT_1:43, A, divfin1;
consider n being Nat such that
D: ( card (MonicDivisors q) = n & n <= 2 |^ (deg q) ) by divfin2;
reconsider q1 = a * q as Element of the carrier of (Polynom-Ring the SplittingField of u) by POLYNOM3:def 10;
deg q = deg q1 by RING_5:4
.= deg u by A, FIELD_4:20 ;
hence card (MonicDivisors p) <= 2 |^ (deg p) by C, D, XXREAL_0:2; :: thesis: verum

end;

suppose A: p is constant ; :: thesis: card (MonicDivisors p) <= 2 |^ (deg p)

now :: thesis: for o being object st o in MonicDivisors p holds
o in {(1_. F)}

let o be object ; :: thesis: ( o in MonicDivisors p implies o in {(1_. F)} )
assume o in MonicDivisors 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)} & card {(1_. F)} = 1 ) by CARD_2:42;
then C: card (MonicDivisors p) <= 1 by NAT_1:43;
deg p = 0 by A, RATFUNC1:def 2;
hence card (MonicDivisors p) <= 2 |^ (deg p) by C, NEWTON:4; :: thesis: verum

end;

end;