let L be Field; :: thesis: for n being Element of NAT
for f being non-zero Polynomial of L st deg f = n holds
ex m being Element of NAT st
( m = card (Roots f) & m <= n )
defpred S₁[ Nat] means for f being non-zero Polynomial of L st deg f = $1 holds
ex m being Element of NAT st
( m = card (Roots f) & m <= $1 );

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for f being non-zero Polynomial of L st deg f = k + 1 holds
ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )

let f be non-zero Polynomial of L; :: thesis: ( deg f = k + 1 implies ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) )
A3: f <> 0_. L by UPROOTS:def 5;
assume A4: deg f = k + 1 ; :: thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )
thus ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) :: thesis: verum

proof

per cases ( Roots f = {} or Roots f <> {} ) ;

suppose Roots f = {} ; :: thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )

hence ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) ; :: thesis: verum

end;

suppose A5: Roots f <> {} ; :: thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )

set RF = Roots f;
consider z being object such that
A6: z in Roots f by A5, XBOOLE_0:def 1;
reconsider z = z as Element of L by A6;
set g = f div (rpoly (1,z));
A7: z is_a_root_of f by A6, POLYNOM5:def 10;
then rpoly (1,z) divides f by HURWITZ:35;
then 0_. L = f mod (rpoly (1,z)) ;
then (f div (rpoly (1,z))) *' (rpoly (1,z)) = (f - ((f div (rpoly (1,z))) *' (rpoly (1,z)))) + ((f div (rpoly (1,z))) *' (rpoly (1,z))) by POLYNOM3:28;
then (f div (rpoly (1,z))) *' (rpoly (1,z)) = f + ((- ((f div (rpoly (1,z))) *' (rpoly (1,z)))) + ((f div (rpoly (1,z))) *' (rpoly (1,z)))) by POLYNOM3:26;
then (f div (rpoly (1,z))) *' (rpoly (1,z)) = f + (((f div (rpoly (1,z))) *' (rpoly (1,z))) - ((f div (rpoly (1,z))) *' (rpoly (1,z)))) ;
then (f div (rpoly (1,z))) *' (rpoly (1,z)) = f + (0_. L) by POLYNOM3:29;
then A8: f = (f div (rpoly (1,z))) *' (rpoly (1,z)) by POLYNOM3:28;
then f div (rpoly (1,z)) <> 0_. L by A3, POLYNOM3:34;
then reconsider g = f div (rpoly (1,z)) as non-zero Polynomial of L by UPROOTS:def 5;
set RG = Roots g;
deg g = (k + 1) - 1 by A3, A4, A7, HURWITZ:36
.= k ;
then ex m1 being Element of NAT st
( m1 = card (Roots g) & m1 <= k ) by A2;
then A9: (card (Roots g)) + 1 <= k + 1 by XREAL_1:6;
Roots f c= (Roots g) \/ {z}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Roots f or y in (Roots g) \/ {z} )
assume A10: y in Roots f ; :: thesis: y in (Roots g) \/ {z}
then reconsider y1 = y as Element of L ;
y1 is_a_root_of f by A10, POLYNOM5:def 10;
then eval (f,y1) = 0. L by POLYNOM5:def 7;
then (eval (g,y1)) * (eval ((rpoly (1,z)),y1)) = 0. L by A8, POLYNOM4:24;
then A11: (eval (g,y1)) * (y1 - z) = 0. L by HURWITZ:29;

now :: thesis: y in (Roots g) \/ {z}

per cases ( y1 = z or y1 <> z ) ;

suppose y1 = z ; :: thesis: y in (Roots g) \/ {z}

then y in {z} by TARSKI:def 1;
hence y in (Roots g) \/ {z} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose y1 <> z ; :: thesis: y in (Roots g) \/ {z}

then y1 - z <> 0. L by RLVECT_1:21;
then eval (g,y1) = 0. L by A11, VECTSP_1:12;
then y1 is_a_root_of g by POLYNOM5:def 7;
then y1 in Roots g by POLYNOM5:def 10;
hence y in (Roots g) \/ {z} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence y in (Roots g) \/ {z} ; :: thesis: verum

end;

then A12: card (Roots f) <= card ((Roots g) \/ {z}) by NAT_1:43;
card ((Roots g) \/ {z}) <= (card (Roots g)) + (card {z}) by CARD_2:43;
then card ((Roots g) \/ {z}) <= (card (Roots g)) + 1 by CARD_2:42;
then card (Roots f) <= (card (Roots g)) + 1 by A12, XXREAL_0:2;
hence ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) by A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

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

end;

A13: S₁[ 0 ]

proof

let f be non-zero Polynomial of L; :: thesis: ( deg f = 0 implies ex m being Element of NAT st
( m = card (Roots f) & m <= 0 ) )
assume A14: deg f = 0 ; :: thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= 0 )
reconsider x = f . 0 as Element of L ;
A15: f <> 0_. L by UPROOTS:def 5;
A16: f . 0 <> 0. L

proof

assume f . 0 = 0. L ; :: thesis: contradiction
then f = <%(0. L)%> by A14, ALGSEQ_1:def 5;
hence contradiction by A15, POLYNOM5:34; :: thesis: verum

end;

A17: now :: thesis: for z being Element of L holds eval (<%x%>,z) <> 0. L

let z be Element of L; :: thesis: eval (<%x%>,z) <> 0. L
eval (<%x%>,z) = eval (<%x,(0. L)%>,z) by POLYNOM5:43
.= x by POLYNOM5:45 ;
hence eval (<%x%>,z) <> 0. L by A16; :: thesis: verum

end;

A18: f = <%x%> by A14, ALGSEQ_1:def 5;
Roots f = {}

proof

assume Roots f <> {} ; :: thesis: contradiction
then consider z being object such that
A19: z in Roots f by XBOOLE_0:def 1;
reconsider z = z as Element of L by A19;
z is_a_root_of f by A19, POLYNOM5:def 10;
then eval (<%x%>,z) = 0. L by A18, POLYNOM5:def 7;
hence contradiction by A17; :: thesis: verum

end;

hence ex m being Element of NAT st
( m = card (Roots f) & m <= 0 ) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A13, A1);
hence for n being Element of NAT
for f being non-zero Polynomial of L st deg f = n holds
ex m being Element of NAT st
( m = card (Roots f) & m <= n ) ; :: thesis: verum