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

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

now

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 set 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 9;
then rpoly 1,z divides f by HURWITZ:35;
then 0_. L = f mod (rpoly 1,z) by HURWITZ:def 7;
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:29;
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:30;
then A8: f = (f div (rpoly 1,z)) *' (rpoly 1,z) by POLYNOM3:29;
then f div (rpoly 1,z) <> 0_. L by A3, POLYNOM3:35;
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:8;
Roots f c= (Roots g) \/ {z}

proof

let y be set ; :: 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 9;
then eval f,y1 = 0. L by POLYNOM5:def 6;
then (eval g,y1) * (eval (rpoly 1,z),y1) = 0. L by A8, POLYNOM4:27;
then A11: (eval g,y1) * (y1 - z) = 0. L by HURWITZ:29;

now

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:35;
then eval g,y1 = 0. L by A11, VECTSP_1:44;
then y1 is_a_root_of g by POLYNOM5:def 6;
then y1 in Roots g by POLYNOM5:def 9;
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:44;
card ((Roots g) \/ {z}) <= (card (Roots g)) + (card {z}) by CARD_2:62;
then card ((Roots g) \/ {z}) <= (card (Roots g)) + 1 by CARD_2:60;
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 6;
hence contradiction by A15, POLYNOM5:35; :: thesis: verum

end;

A17: now

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

end;

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

proof

assume Roots f <> {} ; :: thesis: contradiction
then consider z being set 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 9;
then eval <%x%>,z = 0. L by A18, POLYNOM5:def 6;
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 Element of NAT holds S₁[k] from NAT_1:sch 1(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