let F be Field; :: thesis: for p being Ppoly of F ex n being Nat st
( card (MonicDivisors p) = n & n <= 2 |^ (deg p) )
let p be Ppoly of F; :: thesis: ex n being Nat st
( card (MonicDivisors p) = n & n <= 2 |^ (deg p) )
defpred S₁[ Nat] means for p being Ppoly of F st deg p = $1 holds
ex n being Nat st
( card (MonicDivisors p) = n & n <= 2 |^ (deg p) );

IS: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume IV: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now :: thesis: for p being Ppoly of F st deg p = k holds
ex n being Nat st
( card (MonicDivisors p) = n & n <= 2 |^ (deg p) )

let p be Ppoly of F; :: thesis: ( deg p = k implies ex n being Nat st
( card (MonicDivisors n) = b₂ & b₂ <= 2 |^ (deg n) ) )
assume AS: deg p = k ; :: thesis: ex n being Nat st
( card (MonicDivisors n) = b₂ & b₂ <= 2 |^ (deg n) )
then I: ( k <> 0 & ( k <= 1 implies not not k = 0 & ... & not k = 1 ) ) by RATFUNC1:def 2;
set a = the Element of Roots p;
the Element of Roots p is_a_root_of p by POLYNOM5:def 10;
then consider s being Polynomial of F such that
A: p = (rpoly (1, the Element of Roots p)) *' s by HURWITZ:33;
( rpoly (1, the Element of Roots p) <> 0_. F & s <> 0_. F ) by A;
then E: deg p = (deg (rpoly (1, the Element of Roots p))) + (deg s) by A, HURWITZ:23
.= 1 + (deg s) by HURWITZ:27 ;

per cases ( k = 1 or k > 1 ) by I;

suppose V: k = 1 ; :: thesis: ex n being Nat st
( card (MonicDivisors n) = b₂ & b₂ <= 2 |^ (deg n) )

then ( s is monic & s is constant ) by AS, E, A, ZZ3y, RATFUNC1:def 2;
then s = 1_. F by lemconst;
then MonicDivisors p = {(1_. F),(rpoly (1, the Element of Roots p))} by A, divfin2h;
then card (MonicDivisors p) = 2 |^ (deg p) by AS, V, CARD_2:57;
hence ex n being Nat st
( card (MonicDivisors p) = n & n <= 2 |^ (deg p) ) ; :: thesis: verum

end;

suppose A0: k > 1 ; :: thesis: ex n being Nat st
( card (MonicDivisors n) = b₂ & b₂ <= 2 |^ (deg n) )

now :: thesis: not s is constant

assume s is constant ; :: thesis: contradiction
then 1 + (deg s) <= 1 + 0 by XREAL_1:6, RATFUNC1:def 2;
hence contradiction by A0, AS, E; :: thesis: verum

end;

then ( not s is constant & s is monic ) by A, ZZ3y;
then reconsider s = s as Ppoly of F by A, FIELD_8:10;
set M = { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } ;
set M1 = MonicDivisors s;
set M2 = { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) } ;
C: { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } c= (MonicDivisors s) \/ { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) }

proof

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 (MonicDivisors s) \/ { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) }

let o be object ; :: thesis: ( o in { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } implies b₁ in (MonicDivisors s) \/ { b₂ where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( b₃ divides s & r = (rpoly (1, the Element of Roots p)) *' b₃ ) } )
assume o in { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } ; :: thesis: b₁ in (MonicDivisors s) \/ { b₂ where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( b₃ divides s & r = (rpoly (1, the Element of Roots p)) *' b₃ ) }
then consider q being monic Element of the carrier of (Polynom-Ring F) such that
C1: ( o = q & q divides p ) ;

per cases ( q divides s or ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) ) by C1, A, r59Bag;

suppose q divides s ; :: thesis: b₁ in (MonicDivisors s) \/ { b₂ where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( b₃ divides s & r = (rpoly (1, the Element of Roots p)) *' b₃ ) }

then o in MonicDivisors s by C1;
hence o in (MonicDivisors s) \/ { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) ; :: thesis: b₁ in (MonicDivisors s) \/ { b₂ where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( b₃ divides s & r = (rpoly (1, the Element of Roots p)) *' b₃ ) }

then o in { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) } by C1;
hence o in (MonicDivisors s) \/ { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) } by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } c= (MonicDivisors s) \/ { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) } ; :: thesis: verum

end;

deg s < k by AS, E, NAT_1:13;
then consider n being Nat such that
D: ( card (MonicDivisors s) = n & n <= 2 |^ (deg s) ) by IV;
reconsider M1 = MonicDivisors s as non empty finite set by D;
G: (rpoly (1, the Element of Roots p)) *' (1_. F) is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
(1_. F) *' s = s ;
then 1_. F divides s by RING_4:1;
then (rpoly (1, the Element of Roots p)) *' (1_. F) in { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) } by G;
then reconsider M2 = { q where q is monic Element of the carrier of (Polynom-Ring F) : ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) } as non empty set ;
Z: card M2 = card M1

proof

defpred S₂[ object , object ] means ex u being Polynomial of F st
( $2 = u & $1 = (rpoly (1, the Element of Roots p)) *' u );

D1: now :: thesis: for x being Element of M2 ex y being Element of M1 st S₂[x,y]

let x be Element of M2; :: thesis: ex y being Element of M1 st S₂[x,y]
x in M2 ;
then consider q being monic Element of the carrier of (Polynom-Ring F) such that
E1: ( x = q & ex r being Polynomial of F st
( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) ) ;
consider r being Polynomial of F such that
E2: ( r divides s & q = (rpoly (1, the Element of Roots p)) *' r ) by E1;
r is monic Element of the carrier of (Polynom-Ring F) by E2, ZZ3y, POLYNOM3:def 10;
then r in { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides s } by E2;
hence ex y being Element of M1 st S₂[x,y] by E1, E2; :: thesis: verum

end;

consider f being Function of M2,M1 such that
D2: for x being Element of M2 holds S₂[x,f . x] from FUNCT_2:sch 3(D1);
D3: rng f = M1

proof

now :: thesis: for o being object st o in M1 holds
ex x being object st
( x in M2 & o = f . x )

let o be object ; :: thesis: ( o in M1 implies ex x being object st
( x in M2 & o = f . x ) )
assume o in M1 ; :: thesis: ex x being object st
( x in M2 & o = f . x )
then consider r being monic Element of the carrier of (Polynom-Ring F) such that
E1: ( o = r & r divides s ) ;
(rpoly (1, the Element of Roots p)) *' r is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
then E2: (rpoly (1, the Element of Roots p)) *' r in M2 by E1;
then consider u being Polynomial of F such that
E3: ( f . ((rpoly (1, the Element of Roots p)) *' r) = u & (rpoly (1, the Element of Roots p)) *' r = (rpoly (1, the Element of Roots p)) *' u ) by D2;
thus ex x being object st
( x in M2 & o = f . x ) by E1, E2, E3, RATFUNC1:7; :: thesis: verum

end;

hence rng f = M1 by FUNCT_2:10; :: thesis: verum

end;

D4: dom f = M2 by FUNCT_2:def 1;
f is one-to-one

proof

now :: thesis: for x1, x2 being object st x1 in M2 & x2 in M2 & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in M2 & x2 in M2 & f . x1 = f . x2 implies x1 = x2 )
assume E0: ( x1 in M2 & x2 in M2 & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then consider u1 being Polynomial of F such that
E1: ( f . x1 = u1 & x1 = (rpoly (1, the Element of Roots p)) *' u1 ) by D2;
consider u2 being Polynomial of F such that
E2: ( f . x2 = u2 & x2 = (rpoly (1, the Element of Roots p)) *' u2 ) by E0, D2;
thus x1 = x2 by E0, E1, E2; :: thesis: verum

end;

hence f is one-to-one by FUNCT_2:19; :: thesis: verum

end;

hence card M2 = card M1 by D3, D4, CARD_1:70; :: thesis: verum

end;

then reconsider M2 = M2 as non empty finite set ;
( M1 \/ M2 is finite & { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } c= M1 \/ M2 ) by C;
then reconsider M = { q where q is monic Element of the carrier of (Polynom-Ring F) : q divides p } as finite set ;
F: (card M1) + (card M2) <= (2 |^ (deg s)) + (2 |^ (deg s)) by D, Z, XREAL_1:7;
G: card (M1 \/ M2) <= (card M1) + (card M2) by CARD_2:43;
card M <= card (M1 \/ M2) by C, NAT_1:43;
then H: card M <= (card M1) + (card M2) by G, XXREAL_0:2;
(2 |^ (deg s)) + (2 |^ (deg s)) = (2 |^ (deg s)) * 2
.= 2 |^ (deg p) by E, NEWTON:6 ;
hence ex n being Nat st
( card (MonicDivisors p) = n & n <= 2 |^ (deg p) ) by H, F, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence S₁[k] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(IS);
hence ex n being Nat st
( card (MonicDivisors p) = n & n <= 2 |^ (deg p) ) ; :: thesis: verum